Introducing Proofs of a Program´s Termination in an Undergraduate Software Engineering Course

The author made the first attempt to introduce proofs of program correctness in an undergraduate software engineering course in Fall 2005 at the author´s university. The author also noticed that existing textbooks might cover Hoare´s axioms for proving partial correctness of program without touching proofs of program terminations. In this paper, we are presenting a method for proving a program´s termination. After Hoare´s axioms are applied to a program, the method can be applied to the program to show whether the program terminates successfully with correct outputs. Different techniques for proving program terminations in terms of different loop structures are also discussed. With the introduction of proofs of program terminations to students in a software engineering course, the students can have a full picture of proofs of program correctness. Lastly, we present our experience of teaching proofs of program correctness.