Week 7-8: Program Correctness and Termination

The use of iterative and recursive functions are widely used, but rarely do we prove that a program is correct and produces the correct output for every passable input by some sound argument. In week 7, we looked into the proofs of how preconditions and executions implies the postconditions. When we assume that a program is correct, some assumptions are made and we believe they must be true for every computation at the end of each iteration. This is known as the loop invariant and by stating this, it certainly helps me in understanding the iterative algorithms as a coder and reader. It's important to establish the loop invariant, as well as maintaining it before we exit the loop. In A2, it was definitely some challenege to prove that m = int(mat.sqrt(b*e)) actually worked for binary search, compared to m as the midpoint of the left and right. If m was correct, then indeed everything else would flow. Otherwise, it would be necessary to disprove by a counter example for its program correctness.

The above elements only checks for partial correctness of a program. To further develop a solution, we must also show that the loop terminates at a certain point of the loop. This is known as termination, which we looked at in week 8. I have a feeling it's going to be something big on the upcoming test and I should review more on the material of termination and correctness in the textbook and other examples online.