Proving Program Correctness The Axiomatic Approach What is Correctness Correctness partial correctness termination Partial correctness Program implements its specification Proving Partial Correctness Goal prove that program is partially correct Approach model computation with predicates Predicates are boolean functions over program state Simple example odd x a x odd a Generally P S Q where P precondition Q postcondition S Programming language statement Proof System Two elements of proof system Axioms capture the effect of prog lang stmts Inference rules compose axioms to build up proofs of entire program behavior Let s start by discussing inference rules and then we ll return to discussing axioms Composition Rule P S1 Q Q S2 R P S1 S2 R Consider two predicates odd x 1 x x 1 odd x odd x a x odd a What is the effect of executing both stmts odd x 1 x x 1 a x odd a Consequence 1 Rule Ex P S R R Q P S Q odd x a x odd a and Postcondition a 4 What can we say about this program odd x a x odd a odd a a 4 odd x a x a 4 Consequence 2 Rule Ex P R R S Q P S Q Precondition x 1 and odd x a x odd a What can we say about this program x 1 odd x odd x a x odd a x 1 a x odd a Axioms Axioms explain the effect of executing a single statement Axioms will be derived backwards Start with postcondition and determine what conditions must be true on entry to stmt Assignment Axiom Rule Pyx x y P Replace all free occurences of x with y e g odd x a x odd a Conditional Stmt 1 Axiom Rule P P Bif S Q P Bif Q P if Bif then S Q Bif P Bif P Bif S Q Conditional Stmt 1 Example 1 if even x then 2 x x 1 3 odd x x 3 else part even x odd x x 3 then part odd x 1 x 2 x x 1 odd x x 3 even x odd x 1 x 2 P odd x 1 x 2 x 3 x 3 works as well Conditional Stmt 2 Axiom Rule P P Bif S1 Q P Bif S2 Q P if Bif then S1 else S2 Q Bif P Bif P Bif S1 S2 Q Conditional Stmt 2 Axiom Example 1 if x 0 then 2 x x y x 3 else 4 y x 5 y x Then part x x y x y x x x x x x x x 0 x x Else part x x y x y x x 0 x x P x x x x While Loop Axiom Rule P B S P P while B do S P B P Bif Infinite number of paths so we need one predicate for that captures the effect of S P is called an invariant S P B While Loop Axiom Example IN B 0 a A b B y 0 while b 0 do y y a b b 1 OUT y AB INV y ab AB b 0 Bw b 0 Show INV Bw OUT y ab AB b 0 b 0 y ab AB b 0 y AB So INV Bw OUT Establish IN INV ab AB b 0 y 0 INV aB AB B 0 b B AB AB B 0 a A So IN a A b B y 0 INV While Loop Axiom Need to show INV Bw loop body INV y a b 1 AB b 1 0 b b 1 INV y a a b 1 AB b 1 0 y y a y ab AB b 1 0 loop body INV y ab AB b 0 b 0 y ab AB b 1 0 So IN lines 1 3 INV INV while loop INV Bw and INV Bw OUT Therefore IN program OUT Total correctness After you have shown partial correctness Need to prove that program terminates Usually a progress argument Last program Loop terminates if b 0 b starts positive and is decremented by 1 every iteration So loop must eventually terminate