Hello, dear friend, you can consult us at any time if you have any questions, add WeChat: THEend8_
COMP1600 / COMP6260
Basic Ingredient. Hoare-triples {P} S {Q} P and Q are predicates (formulae) S is a code (fragment) Example. {x > 0} while (x>0) do x := x-1 {x = 0} Meaning. If we run S from a state that satisfies precondition P and if S terminates, then the post-state will satisfy Q. 1 / 49 Hoare Logic Idea. Proof Rules that allow us to prove all true triples. Assignment {Q(e)} x := e {Q(x)} Precondition Strengthening / Postcondition Weakening Ps → Pw {Pw} S {Q} {Ps} S {Q} {P} S {Qs} Qs → Qw {P} S {Qw} Sequence. {P} S1 {Q} {Q} S2 {R} {P} S1; S2 {R} Conditional. {P ∧ b} S1 {Q} {P ∧ ¬b} S2 {Q} {P} if b then S1 else S2 {Q} 2 / 49 Proof Rule for While Loops (Rule 6/6) {I ∧ b} S {I} {I} while b do S {I ∧ ¬b} I is called the loop invariant. I is true before we encounter the while statement, and remains true each time around the loop (although not necessarily midway during execution of the loop body). If the loop terminates the control condition must be false, so ¬b appears in the postcondition. For the body of the loop S to execute, b needs to be true, so it appears in the precondition. 3 / 49 Soundness of the While Rule w.r.t. the semantics {I ∧ b} S {I} {I} while b do S {I ∧ ¬b} Soundness. If the premise is true, then so is the conclusion. assume that I holds in the initial state. if b is false, nothing happens, so I ∧ ¬b is true in post-state. if b is true, then (by premise) I holds at end of each iteration assuming that the loop terminates, b becomes false (and I still holds) Q. What about non-termination? 4 / 49 Applying the While Rule {I ∧ b} S {I} {I} while b do S {I ∧ ¬b} {P} while b do S {Q} Difficult bit. Finding the right invariant. This requires intuition and practice. There is no automated way of doing this. Easy bit. Establishing the desired postcondition The postcondition we get after applying our rule has form I ∧ ¬b. But if I ∧ ¬b → Q, we can use postcondition weakening. Easy bit. Establishing the desired precondition The precondition we get after applying our rule has form I . But if P → I , we can use precondition strengtening. 5 / 49 Applying the While Rule (schematic proof) {I ∧ b} S {I} {I} while b do S {I ∧ ¬b} {P} while b do S {Q} 1. {I ∧ b} S {I} 2. {I} while b do S {I ∧ ¬b} (While Loop, 1) 3. I ∧ ¬b → Q (Logic) 4. {I} while b do S {Q} (Postcondition Weakening, 2, 3) 5. P → I (Logic) 6. {P} while b do S {Q} (Precondition Strengthening, 4, 6) 6 / 49 Applying the While Rule (schematic proof) {I ∧ b} S {I} {I} while b do S {I ∧ ¬b} {P} while b do S {Q} 1. {I ∧ b} S {I} 2. {I} while b do S {I ∧ ¬b} (While Loop, 1) 3. I ∧ ¬b → Q (Logic) 4. {I} while b do S {Q} (Postcondition Weakening, 2, 3) 5. P → I (Logic) 6. {P} while b do S {Q} (Precondition Strengthening, 4, 6) 6 / 49 Applying the While Rule (schematic proof) {I ∧ b} S {I} {I} while b do S {I ∧ ¬b} {P} while b do S {Q} 1. {I ∧ b} S {I} 2. {I} while b do S {I ∧ ¬b} (While Loop, 1) 3. I ∧ ¬b → Q (Logic) 4. {I} while b do S {Q} (Postcondition Weakening, 2, 3) 5. P → I (Logic) 6. {P} while b do S {Q} (Precondition Strengthening, 4, 6) 6 / 49 Applying the While Rule (schematic proof) {I ∧ b} S {I} {I} while b do S {I ∧ ¬b} {P} while b do S {Q} 1. {I ∧ b} S {I} 2. {I} while b do S {I ∧ ¬b} (While Loop, 1) 3. I ∧ ¬b → Q (Logic) 4. {I} while b do S {Q} (Postcondition Weakening, 2, 3) 5. P → I (Logic) 6. {P} while b do S {Q} (Precondition Strengthening, 4, 6) 6 / 49 Applying the While Rule (schematic proof) {I ∧ b} S {I} {I} while b do S {I ∧ ¬b} {P} while b do S {Q} 1. {I ∧ b} S {I} 2. {I} while b do S {I ∧ ¬b} (While Loop, 1) 3. I ∧ ¬b → Q (Logic) 4. {I} while b do S {Q} (Postcondition Weakening, 2, 3) 5. P → I (Logic) 6. {P} while b do S {Q} (Precondition Strengthening, 4, 6) 6 / 49 Applying the While Rule (schematic proof) {I ∧ b} S {I} {I} while b do S {I ∧ ¬b} {P} while b do S {Q} 1. {I ∧ b} S {I} 2. {I} while b do S {I ∧ ¬b} (While Loop, 1) 3. I ∧ ¬b → Q (Logic) 4. {I} while b do S {Q} (Postcondition Weakening, 2, 3) 5. P → I (Logic) 6. {P} while b do S {Q} (Precondition Strengthening, 4, 6) 6 / 49 Applying the While Rule (schematic proof) {I ∧ b} S {I} {I} while b do S {I ∧ ¬b} {P} while b do S {Q} 1. {I ∧ b} S {I} 2. {I} while b do S {I ∧ ¬b} (While Loop, 1) 3. I ∧ ¬b → Q (Logic) 4. {I} while b do S {Q} (Postcondition Weakening, 2, 3) 5. P → I (Logic) 6. {P} while b do S {Q} (Precondition Strengthening, 4, 6) 6 / 49 Applying the While Rule (schematic proof) {I ∧ b} S {I} {I} while b do S {I ∧ ¬b} {P} while b do S {Q} 1. {I ∧ b} S {I} 2. {I} while b do S {I ∧ ¬b} (While Loop, 1) 3. I ∧ ¬b → Q (Logic) 4. {I} while b do S {Q} (Postcondition Weakening, 2, 3) 5. P → I (Logic) 6. {P} while b do S {Q} (Precondition Strengthening, 4, 6) 6 / 49 Applying the While Rule (schematic proof) {I ∧ b} S {I} {I} while b do S {I ∧ ¬b} {P} while b do S {Q} 1. {I ∧ b} S {I} 2. {I} while b do S {I ∧ ¬b} (While Loop, 1) 3. I ∧ ¬b → Q (Logic) 4. {I} while b do S {Q} (Postcondition Weakening, 2, 3) 5. P → I (Logic) 6. {P} while b do S {Q} (Precondition Strengthening, 4, 6) 6 / 49 Applying the While Rule (schematic proof) {I ∧ b} S {I} {I} while b do S {I ∧ ¬b} {P} while b do S {Q} 1. {I ∧ b} S {I} 2. {I} while b do S {I ∧ ¬b} (While Loop, 1) 3. I ∧ ¬b → Q (Logic) 4. {I} while b do S {Q} (Postcondition Weakening, 2, 3) 5. P → I (Logic) 6. {P} while b do S {Q} (Precondition Strengthening, 4, 6) 6 / 49 Applying the While Rule (schematic proof) {I ∧ b} S {I} {I} while b do S {I ∧ ¬b} {P} while b do S {Q} 1. {I ∧ b} S {I} 2. {I} while b do S {I ∧ ¬b} (While Loop, 1) 3. I ∧ ¬b → Q (Logic) 4. {I} while b do S {Q} (Postcondition Weakening, 2, 3) 5. P → I (Logic) 6. {P} while b do S {Q} (Precondition Strengthening, 4, 6) 6 / 49 Applying the While Rule (schematic proof) {I ∧ b} S {I} {I} while b do S {I ∧ ¬b} {P} while b do S {Q} 1. {I ∧ b} S {I} 2. {I} while b do S {I ∧ ¬b} (While Loop, 1) 3. I ∧ ¬b → Q (Logic) 4. {I} while b do S {Q} (Postcondition Weakening, 2, 3) 5. P → I (Logic) 6. {P} while b do S {Q} (Precondition Strengthening, 4, 6) 6 / 49 Example Goal. Find condition I to prove that: {n > 3} while n>0 do n := n-1 {n = 0} Observation. Need to prove the above using while-rule, i.e. {I ∧ b} n := n− 1 {I} {I} while (n>0) do n:= n-1 {I ∧ n ≤ 0} Want. Loop invariant I such that It is implied by the precondition: n > 3→ I if the loop terminates (i.e. n > 0 is false), then I should imply the postcondition: I ∧ n ≤ 0→ n = 0 If I is true and the body is executed, I is true afterwards: {I ∧ n > 0} n := n− 1 {I} Loop Invariant. I ≡ (n ≥ 0) have {n ≥ 0 ∧ n > 0} n := n− 1 {n ≥ 0} n ≥ 0 ∧ ¬(n > 0)→ n = 0 7 / 49 Example (cont.) Goal. Find condition I to prove that: {n > 3} while n>0 do n := n-1 {n = 0} Loop Invariant. I ≡ (n ≥ 0), we have n > 3→ n ≥ 0, n ≥ 0 ∧ n ≤ 0→ n = 0, and {n ≥ 0 ∧ n > 0} n := n− 1 {n ≥ 0}. 7 / 49 Example, Formally 1. {n − 1 ≥ 0} n := n− 1 {n ≥ 0} (Assignment) 2. n ≥ 0 ∧ n > 0→ n − 1 > 0 (Logic) 3. {n ≥ 0 ∧ n > 0} n := n− 1 {n ≥ 0} (Prec. Strength., 1, 2) 4. {n ≥ 0} while (n > 0) do n := n− 1 {n ≥ 0∧¬(n > 0)} (While Loop, 3) 5. n > 3→ n ≥ 0 (Logic) 6. {n > 3} while (n > 0) do n := n− 1 {n ≥ 0 ∧ ¬(n > 0)} (Prec. Strength., 4, 5) 7. n = 0↔ n ≥ 0 ∧ ¬(n > 0) (Logic) 8. {n ≥ 0} while (n > 0) do n := n− 1 {n = 0} (Post. Equiv., 6, 7) Other Invariants e.g. true or n = 0 both are invariants, and give n = 0 as postcondition but n ≥ 0 is better (weaker) as it is more general. 8 / 49 Let’s Prove a Program! Program (with specification): {True} i:=0; s:=0; while (i ̸= n) do i:=i+1; s:=s+(2*i-1) {s = n2} (The sum of the first n odd numbers is n2) Goal: prove {True} Program {s = n2} 9 / 49 A Very Informal Analysis Let’s look at some examples: 1 = 1 = 12 1 + 3 = 4 = 22 1 + 3 + 5 = 9 = 32 1 + 3 + 5 + 7 = 16 = 42 . . . It looks OK - let’s see if we can prove it! Goal: prove {True} Program {s = n2} 10 / 49 How can we prove it? First Task. Find a loop invariant I . (NB: S and s are different!) Post condition and loop condition: {I ∧ b} S {I} {I} while b do S {I ∧ ¬b} while (i ̸= n) do i:=i+1; (1, 2, 3, ...) s:=s+(2*i-1) (1, 4, 9, ...) {s = n2} Want. (I ∧ i = n)→ (s = n2) to apply postcondweak Loop Body. Each time i increments, s moves to next square number. Invariant. I ≡ s = i2. 11 / 49 Check I as (s = i2) is an invariant: prove {I}S{I} {s = i2} i := i + 1 {Q} {Q} s := s + (2 ∗ i − 1) {s = i2} Seq{s = i2} i := i + 1; s := s + (2 ∗ i − 1) {s = i2} Using the assignment axiom and the sequence rule: 1. {Q} s:=s+(2*i-1) {s = i2} 2. 3. {s = i2} i:=i+1 {Q} 4. {s = i2} i:=i+1; s:=s+(2*i-1) {s = i2} (Sequence, 3, 1) 12 / 49 Check I as (s = i2) is an invariant: prove {I}S{I} {s = i2} i := i + 1 {Q} {Q} s := s + (2 ∗ i − 1) {s = i2} Seq{s = i2} i := i + 1; s := s + (2 ∗ i − 1) {s = i2} Q is {s + (2 ∗ i − 1) = i2} Using the assignment axiom and the sequence rule: 1. {s + (2 ∗ i − 1) = i2} s:=s+(2*i-1) {s = i2} (Assignment) 2. 3. {s = i2} i:=i+1 {s + (2 ∗ i − 1) = i2} 4. {s = i2} i:=i+1; s:=s+(2*i-1) {s = i2} (Sequence, 3, 1) 13 / 49 Check I as (s = i2) is an invariant: prove {I}S{I} {s = i2} i := i + 1 {Q} {Q} s := s + (2 ∗ i − 1) {s = i2} Seq{s = i2} i := i + 1; s := s + (2 ∗ i − 1) {s = i2} Q is {s + (2 ∗ i − 1) = i2} Using the assignment axiom and the sequence rule: 1. {s + (2 ∗ i − 1) = i2} s:=s+(2*i-1) {s = i2} (Assignment) 2. {s + (2 ∗ (i + 1)− 1) = (i + 1)2} i:=i+1 {s + (2 ∗ i − 1) = i2} (Assignment) 3. {s = i2} i:=i+1 {s + (2 ∗ i − 1) = i2} (Prec. Equiv., 2) 4. {s = i2} i:=i+1; s:=s+(2*i-1) {s = i2} (Sequence, 3, 1) So far, so good. (I as (s = i2) is an invariant.) 14 / 49 Completing the Proof of {True} Program {s = n2} 6 Strengthen the precondition to match the While rule premise {I ∧ b} S {I} {(s = i2) ∧ (i ̸= n)} i:=i+1; s:=s+(2*i-1) {s = i2} 7 Apply the While rule and postcondition equiv: s = i2 ∧ i = n↔ s = n2 {s = i2} while ... s:=s+(2*i-1) {s = n2} 8 Check that the initialisation establishes the invariant: {0 = 02} i:=0 {0 = i2} {0 = i2} s:=0 {s = i2} {0 = 02} i:=0; s:=0 {s = i2} 9 (0 = 02) ↔ True, so putting it all together with Sequencing we have {True} i := 0 ; s := 0 ; while (i ̸= n) do S {s = n2} 15 / 49 What about Termination? Hoare Logic (in this form) proves partial correctness. Example. while 1+1 = 2 do x:=0. This will loop forever! can still prove things about it Exercise. {True} while 1+1 = 2 do x:=0 {False} Termination. remember functional programs? Something must decrease need loop variant (later) 16 / 49 Are the Rules Complete? So far. Have a very simple language new rules for arrays, for-loops, exceptions, . . . Focus here. Soundness every provable Hoare triple is (semantically) true soundness holds but terms and conditions apply with these assumptions, also have completeness, i.e. every true Hoare triple is provable. Completeness. if {P} S {Q} is true then {P} S {Q} is provable 17 / 49 What are these Assumptions? The language we use for expressions in our programs is the same as the language we use in our pre- and postconditions (in our case, basic arithmetic). We assumed no aliasing of variables. (In most real languages we can have multiple names for the one piece of memory.) How is aliasing a problem? Suppose x and y refer to the same cell of memory. ▶ We get {y +1 = 5 ∧ y = 5} x:=y+1 {x = 5 ∧ y = 5} (Assignment) ▶ i.e. {y = 4 ∧ y = 5} x:=y+1 {x = 5 ∧ y = 5} ▶ i.e. if initial state satisfies False and x:=y+1 terminates then final state satisfies {x = 5 ∧ y = 5} (but also works for x = 6 ∧ y = 6) which makes a mockery of our calculus since it proves rubbish!