Proof iteration vs Proof recursion

So I learned some flavors of induction, it is time to apply them into something familiar. Iteration and recursion.

Recall when designing a iteration part of a program, I worry about if the result is what I want, i worry about if the loop enters an infinite loop. When trying to prove an iteration correct, we need to prove that every time the loop goes through, it is partially correct. In addition, we need to prove that the loop terminates.
To prove partial correctness, it is convenient to prove a loop invariant, which is always right after each iterating. I should take notice that a loop invariant can be any condition. Like the 2nd question in test2, where the loop invariant is simply that n is always a natural number. To prove termination, recall PWO which lead to a theorem which says that every decreasing sequence of natural numbers is finite. So I have to find the decreasing sequence. This may or may not be the same as the loop invariant, but it has to be decreasing, and consists of all natural numbers.

This is a rush exam period, so I have to remind myself not to get confused with the prove of recursive programs. In recursion we do not usually have an invariant, since every time the program calls itself, it has no record of how many steps it actually went though.(Unless we set a stack or other way.) However, recall when I was learning writing recursion program in CSC148, the first thing I was told was that a recursion has to have a base case, otherwise the recursion never terminates. So recursive program is actually an inductively defined program. Then proving recursion correctness is in the similar way as we write induction for inductive defined predicates. We first prove that the base case is correct, then using some flavor of induction to prove that P(n) holds for all n. The if statements are good signs of separating cases.