Week 7

Proving correctness of a program is an interesting concept. Rather than the way we have been taught to check our code (through test cases), we now define preconditions and postconditions to see if they work every time the program is recursively called. I wonder if this would be too complex of a proof for one of our 207 assignments in order to avoid writing test cases. The concept itself is very interesting, yet the proofs themselves don't seem to be. Oh well.

The problem set was very straightforward. Probably one of the easier ones so far but it's always the stupid silly mistakes that make me lose marks. The only difficulties I encountered are determining what is a sufficient for these (non-numerical) proofs. I find I have to define what something like

# Postcondition: revString(s) returns a string with
# the characters of s in reverse order.

What does reverse order mean? If I am the one deciding it, can I just say reverse order is defined as:

revString(s[1:]) + s[0]