Proving Program Correctness

So I must say I've been pretty much out of tune lately. I find myself having huge problems trying to cope with the work level and the amount of studying time required. I'm totally worn out and I'm pretty sure many of us are also due to many assignments due along with midterms/tests.

I have however, been able to catch up to what Danny's been teaching lately about Program Correctness. For once I understood what is actually going on and that it appeared to be intuitive to me. The proof is more or less an examination of each line of code and proving how given the expected input, the code will generate a proper output. In some cases, the program is expected to handle errors. In the example of Binary Search which Danny has shown in his lecture, if the item is not found, a message "not found" is expected instead of crashing.

Today's lecture is the complement of this idea. It extends proving correctness to loop invariants. The key point emphasized during the lecture was "precondition and termination implies partial correctness". When Danny first said it, It did not appear to be trivial to me as it seems correct if I have a precondition and I can prove that a recursive function will eventually terminate. The example that Danny used regarding "10, 7, 5" as being numbers inside an array helped me understand this fact since a student in class claimed that given Ei = y - bi, as y approaches bi, it will be 0 and it terminates (which at first seem very convincing).