Urban Hafner

CTM: Exercises of Chapter 1 (Exercise 3)

Posted by urban Sat, 02 Apr 2005 11:32:00 GMT

The problem

Program correctness. Section 1.6 explains the basic ideas of program correctness an applies them to show that the factorial function defined in section 1.3 is correct. In this exercise, apply the same ideas to the function Pascal of section 1.5 to show that it is correct.

My solution

I must admit that I have never been very confident when proving things. So take the following prove with a grain of salt and don’t assume that it is good style to be so sloopy.

• {Pascal 1} is correct as it returns [1].
• Assume that {Pascal N-1} is correct (and assume that AddList, ShiftLeft and ShiftRight are correct, too).

To calculate the n-th row of Pascal’s triangle you take the (n-1)-th row and prepend 0 on the left and you take the (n-1)-th row (again) and append 0 on the right. Then you just add the two lists (i.e. the corresponding elements of the two rows) and you have the n-th row of Pascal’s triangle. This is just what Pascal does.

q.e.d.