Seveth Week - Program Correctness

Program correctness is based on preconditions and postconditions. Programs basically establish a contract with the user: so long as they supply the correct input that satisfies the precondition, the program will generate the correct output according to the postconditions. Obviously, in order to make programs as flexible as possible, we naturally want to have as weak preconditions as possible, while having very rigid postconditions. A counterproof for program correctness finds valid input that generate invalid output. A proof for program correctness must show that if the precondition is assumed, then the postcondition is true.

We also took a look at programs that calculate the greatest common denominator, and calculating powers. Of particular interest was the powers program:

def pow(n,m):
if m = 0 : return 1
else: pow(pow(n, floor(m/2)),2) * pow(n, m%2)

That else condition checks that if m is an odd number, the parts of m ignored by the integer division (floor) will be compensated for. I liked this particular form because I would have thought to use if statements to break m into cases, even or odd. But since multiplying by 1 has no effect on the returned value, and m%2 = 0 will return 1, the need for if statements is eliminated.

EDIT: I'm not sure if I copied 'pow(pow(n, floor(m/2)),2) ' correctly; this seems to give me recursive errors in Python when I try to implement it with simple integer divison to replace the floor functions. Have to take a closer look at this if I have time later on.