Recursive and iterative correctness of functions.

Since inductions and recursive functions can both be expressed recursively, it is reasonable to prove the recursive correctness of a function using induction techniques. Iterative correctness, however, is much harder to prove. We have to first come up with loop invariants. We then have to prove the invariants are true using simple induction and the partial correctness of a function comes as a corollary. Finally, we have to prove that the loop terminates using principle of well-ordering.

Here is a problem I used to practise the recursive correctness of a function.

def maxnum(L):
"""Return the largest number from non-empty list of numbers L """
1. if len(L) == 1 : return L[0]
2. if L[0] > maxnum(L[1:]) : return L[0]
3. return maxnum(L[1:])

Prove P(1):Since n = 1, the list L is of length 1. This satisfies the condition len(L) == 1 at line 1 in the function maxnum(L). Thus, maxnum(L) returns L[0], which is the first and only number in the list. As a result, maxnum(L) returns the largest number in L when L has the length 1. Therefore, P(1) is true.

Prove \forall n \in N\{0}, P(n) \implies P(n+1):

Assume n \in N\{0} and assume that P(n) is correct. Then for any list L of length n, maxnum(L) returns the largest number in L. Assume L' is any list of length n+1, meaning it contains n+1 elements. Then L'[1:] is a list of length n and maxnum(L'[1:]) returns the largest number in L'[1:] by assumption.Then L'[0] > maxnum(L'[1:]) or L'[0] <= maxnum(L'[1:]).

Case 1: assume L'[0] > maxnum(L'[1:]). Then the condition at line 2 in maxnum(L) is satisfied. Then maxnum(L) returns L'[0], which is the largest number in L'since L'[0] > maxnum(L'[1:]) means that L'[0] is greater than any number in L'[1:], which implies that L'[0] is the largest number in L'.

Case 2: assume L'[0] <= maxnum(L'[1:]). Then the condition at line 1 and line 2 in maxnum(L) both dissatisfied. Then line 3 in maxnum(L) is executed and (L) returns maxnum(L'[1:]), which is the largest number in L'since L'[0] <= maxnum(L'[1:]) means that maxnum(L'[1:]) is greater than or equal to L[0], which implies that maxnum(L'[1:]) represents the largest value in L'.
Then maxnum(L) returns the largest number in L'. Then for any list L' of length n+1, maxnum(L') returns the largest number in L'. So P(n+1) is true. P(n) \implies P(n+1). \forall n \in N\{0}, P(n) \implies P(n+1)

Since P(1) \and \forall n \in N\{0}, P(n) \implies P(n+1) is true, we can conclude, by PSI, that \forall n \in N\{0}, P(n).