3/10/10 1 Proving Program Correctness The Axiomatic Approach What is Correctness? • Correctness: – partial correctness + termination • Partial correctness: – Program implements its specification3/10/10 2 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 is a precondition – Q is a postcondition – S is a set of programming language statements Proof System • Two elements of proof system • Axioms – Capture the effect of individual programming language statements • Inference rules – Compose the effect of individual statements and extrinsic knowledge to build up proofs of entire program3/10/10 3 Axioms • Axioms explain the effect of executing a single statement – Assignment – If – If then else – While loop Assignment Axiom • Rule: • Application: Replace all free occurences of x with y – e.g., {odd(x)} a = x {odd(a)3/10/10 4 Inference Rules • Inference rules allow us to compose the effects of individual statements and extrinsic knowledge to build up proofs of entire program • 3 inference rules – Composition – Consequence 1 – Consequence 2 Composition • Rule: • Consider two predicates – {odd(x)} a = x {odd(a)} – {odd(x+1)} x = x+1 {odd(x)} • What is the effect of executing both stmts? – {odd(x+1)} x = x+1 ; a = x {odd(a)}3/10/10 5 Consequence 1 • Rule • Ex: – {odd(x)} a = x {odd(a)} and – Postcondition Q ≡ {a ≠ 4} • What can we say about this program? Consequence 2 • Rule: • Ex: – Precondition P ≡ {x=1} and – {odd(x)} a = x {odd(a)} • What can we say about this program?3/10/10 6 Axioms (cont.) • Axioms explain the effect of executing a single statement – Assignment – If – If then else – While loop Assignment Axiom • Rule: • Application: Replace all free occurences of x with y – e.g., {odd(x)} a = x {odd(a)}3/10/10 7 if Axiom • Rule: Bif S {P} {P ∧ ¬Bif} {P ∧ Bif } {Q} Application • Example: 1. if even(x) then { 2. x = x +1 3. } {odd(x) ∧ x > 3} • else part: need to show {(P ∧ ¬even(x)) ⇒ (odd(x) ∧ x>3)} {P ⇒ (x>3)} • then part: need to show {P ^ even(x)} x=x+1 {odd(x) ∧ x>3} {odd(x+1) ∧ x>2} x = x+1 {odd(x) ∧ x > 3} {(P ∧ even(x)) ⇒ (odd(x+1) ∧ x>2)} {P ⇒ (x>2)} • Need to choose a predicate P consistent with implications above • P ≡ x>2 – x > 39 works as well3/10/10 8 if then else Axiom • Rule {P} {P ∧ ¬Bif} {Q} S2 S1 {P ∧ Bif } Bif Conditional Stmt 2 Axiom • Example: 1. if x < 0 then { 2. x = -x; 3. y = x 4. } else { 5. y = x 6. } {y = |x|} • Then part: need to show {P ∧ (x<0)} x=-x;y=x {y = |x|} {x = |x|} y = x {y = |x|} {-x = |x|} x = -x {x = |x|} ( P ∧ x <0) ⇒ -x = |x| • Else part: need to show {P ∧ ¬ (x<0)} y=x {y = |x|} {x =|x|} y=x {y=|x|} ( P ∧ ¬(x < 0)) ⇒ x = |x| • P ≡ true3/10/10 9 While Loop Axiom • Rule • Infinite number of paths, so we need one predicate for that captures the effect of 0 or more loop traversals • P is called a loop invariant € {P ∧ B} S {P} {P} while B do S {P ∧ ¬B}Bif S {P} {P ∧ ¬B} Proving Partial Correctness • Handle termination separately • Axioms and inference rules are applied in reverse during proof – Start with postcondition and work backwards to determine what must precondition must be3/10/10 10 Partial Correctness Proof IN ≡ {B ≥ 0} a = A b = B y = 0 while b > 0 do { y = y + a b = b - 1 } OUT ≡ {y = AB} While Loop IN ≡ {B ≥ 0} a = A b = B y = 0 while b > 0 do { y = y + a b = b - 1 } OUT ≡ {y = AB} • From while loop axiom need to show {P∧B} S {P} • P ≡ y + ab = AB ∧ b ≥ 0 • Bw ≡ b > 0 • {y + ab = AB ∧ b ≥ 0} y=y+a; b=b-1 {P} • {y+a(b-1) = AB ∧ b-1 ≥ 0} b = b - 1 {P} • {y+a+a(b-1) = AB ∧ b-1 ≥ 0} y = y+a {….} • {y +ab = AB ∧ b-1 ≥ 0} loop body {P} • {y + ab = AB ∧ b ≥ 0 ∧ b > 0} • ⇒ {y +ab = AB ∧ b-1 ≥ 0} • From while loop axiom can conclude {P} while loop {P∧¬ Bw}3/10/10 11 While Loop IN ≡ {B ≥ 0} a = A b = B y = 0 while b > 0 do { y = y + a b = b - 1 } OUT ≡ {y = AB} • Now need to show P ∧ ¬ Bw ⇒ OUT • P ≡ y + ab = AB ∧ b ≥ 0 • Bw ≡ b > 0 • y + ab = AB ∧ b ≥ 0 ∧ ¬(b > 0) • y + ab = AB ∧ b = 0 • y = AB • So {P ∧ ¬ Bw} ⇒ OUT • From consequence rule we can conclude {P} while loop {OUT} While Loop IN ≡ {B ≥ 0} a = A b = B y = 0 while b > 0 do { y = y + a b = b - 1 } OUT ≡ {y = AB} • P ≡ y + ab = AB ∧ b ≥ 0 • Establish {IN} a=A;b=B;y=0 {P} • {ab = AB ∧ b ≥ 0} y=0 { P} • {aB = AB ∧ B ≥ 0} b = B {….} • {AB = AB ∧ B ≥ 0} a = A {….} • So {IN} a=A;b=B;y=0 {P}3/10/10 12 While Loop Axiom • So – {IN} lines 1-3 {P}, – {P} while loop {P ∧ ¬ Bw }, and – {P ∧ ¬ Bw} ⇒ OUT • Therefore – {IN} program {OUT} Total correctness • After you have shown partial correctness – Need to prove that program terminates • Usually a progress argument. For previous program – Loop terminates if b ≤ 0 – b starts positive and is decremented by 1 every iteration – So loop must eventually terminate3/10/10 13 Now You Try It r = 1; i = 0; while i < m do { r = r * n; i = i + 1 } Postcondition: r =