week.seven

reminder: problem set #4 due on friday!

on monday, prof. heap was m.i.a. - something to do with heffalumps? but we kick-started on a new, familiar (from 165) topic: program correctness. basically, a program consists of two things: a precondition ("correct input"; the statement that expresses what the correct input is) and a postcondition (symmetrically the "correct output"). i think in this course we focus our attention on programs that involve some sort of iterative conventions (recursion and loops) - i think it'd be fun discussing what constitutes a loop/recursion and how they really behave. we started by going through the codes for a recursive binary seach. in essence, to prove that the program for recBS works is to show that the precondition: 1 <= index of first element <= index of the last element <= the length of the array and the array is sorted, implies the postcondition: return index i such that first index <= i <= last element and that the element of the array at index i is the element sought after - if such i exists, return 0 or an error message otherwise. and the flavour of induction of use is the pci.

on wednesday, when danny came back, he went over the proof of correctness of recursive binary search. unfortunately, i was late for class - just in time for a new topic to talk about (sigh). we also proved the greatest common divisor using the remainder lemma. when i looked at the whole proof on the lecture slides at first, it was pretty intimidating because there were cases to be taken of and it just looked too complex for my frail proving brain. i might have to do some readings off of the course notes to better understand it.


on friday, we continued on with proving the greatest common divisor program with parameter n and m. more specifically, we proved the following claim:
P(m): \forall n \in N, n > m \implies egcd(n, m) returns gcd(n, m)
Claim: \forall m \in N, P(m)
We carried out the poof using simple induction on m. what was important to me the most from this lecture is the method of using proven results (lemmas) to carry out a proof that (may) have some commonality with the lemma(s) so the proof becomes shorter and easier to read (i suppose).