week.eight

on monday, we discussed the topic of 'named repetition'. essentially, if a function has no loop/recursion, we can trace the sequence of statements one by one and prove that it is correct by stating the return value. otherwise, if the function contains a loop, then there exists a loop invariant that works as an indicator of the loop's iterations and it is true for every iteration of the loop. there are two things to prove when proving a program with loop(s): partial correctness and termination. we applied this to proving a program on power/exponents as an example. as it turns out, a loop invariant helps to prove partial correctness, but proving loop invariant itself may not depend on the postcondition (usually precondition, though). in the end, a correct iterative/recursive program means that the precondition implies the postcondition.

on wednesday, we continued on with our pow program. partial correctness is pretty much works like proving by simple induction (using the loop invariant), and to prove that the loop (and consequently the program) terminates is to find a (strictly) decreasing sequence such that i is the loop index and prove that E_(i+1) < E_i. what i thought the hardest part in proving an iterative program is finding a suitable loop invariant, because they could be anything and one is better than the other - the challenge is finding one that is the best. one thing for sure that i find is that the expression(s) in the loop invariant will involve some (if not all) the program's variable - but it is also important that we don't use these variables explicitly in the induction, rather set the variale, say v, as v_i, where v_i is the value of v in the ith iteration.

on friday, i was late =D. i shall refer to the course slide to catch up (hopefully).