Program Correctness

Termination

How do you show that a program will terminate for sure?

• You can just have a while true loop running forever, but how do you know for sure that it will run forever? the while true case is trivial, but think about more complex problemsc

There is this concept of bounding functions. So you find a bounding function to make sure that the problem will terminate.

To show termination, we identify an integer expression involving the variables of the loop condition whose value:

1. is always greater than or equal to 0,
2. decreases with every loop iteration, and
3. makes the loop’s guard become false as it approaches 0.

To show a recursive function or procedure terminates:

1. Determine a bounding function (an integer expression) involving the arguments to the function or procedure that is non-negative and decreases in each recursive call.
2. Show there is a section of the function or procedure that does not make recursive calls and is entered as this bounding function approaches 0.

• Complexity Theory
• Decision Problem Unsolvable Problems: Decision problems for which no algorithm can exist, i.e. there cannot exist an algorithm to solve the problem.

Lambda Calculus Turing Machine