CS105  Proof Techniques

Proofs w/ recursive functions without changing variables
Show that:
1) Rules in the program are equivalent to the mathematical facts
2) Recursive function calls all meet the function's precondition
3) Each recursive call is simpler, eventually reducing to the base case

  	(example w/ recursive fibonacci function)


Proofs w/ changing variables
A) Add subscripts to the variables:
	 0 for the initial values of parameters,
	 higher numbers for each new assignment in the program text
B) Add correct subscripts to each variable use
A and B convert a program into a form called  "Static Single Assignment" (SSA) form
C) Each subscripted variable has a unique value, so we can use standard proof techniques

 	 (example with showing that two swap functions both swap correctly)


Proofs w/ if
A) Create variables after the "if", annotate them with the values they get in each condition
B) Do proof by cases

 	(example with "sorting" x and y so that x <= y)


Proofs w/ loops
A) Find a rule that remains true as the values of the variables change (a "loop invariant")
B) Show that the following are true:
1) The invariant will be true when we first enter the loop
 	(i.e. the stuff before the loop works)
2) The body of the loop maintains the invariant
	(i.e. the body of the loop works)
3) After the loop, the invariant gives you what you want
4) If we skip the loop, we still get what we want after the loop
5) The loop makes something simpler, eventually reaching a case that stops the loop

	(example w/ loop-based fibonacci function)