assert(p!=null); *p = 10; assert(0<=i && i<buffersize); buffer[i]=10;
int bar(int n) { local int k, int j; k := 0; j := 1; while (k!= n) { k := k + 1; j := 2 + j; } return(j); } 1+2n } { n>0
precondition Hoare Triple {P }S{Q} program statement postcondition C. A. R. Hoare
{P }S{Q} precondition statement postcondition {x 0 y 0} z := x + y {z 0} {x 0 y 0} z := x + y {z 0 x 0 y 0} {x =5 y =2} z := x + y {x =5 z =7} {n 0 n 2 > 28} m := n + 1; m := m m { (m = 36)} { i.a[i] = 10 k 0} a[k] =0 { i.a[i] = 10 k 0} F M invalid
{Q[E/x]} x := E {Q} } { {y +7> 42} x := y +7{x >42} {y = y +7 7 y + 7 = 18} x := y +7{y = x 7 x = 18} } { {P } x := E {P [x /x] (x = E[x /x])} {y = x + 10 x =1} x := y {y = x + 10 x =1 x := x + 10}
{P } S 1 {R} {R} S 2 {Q} {P } S 1 ; S 2 {Q} } { {y + z > 4} y := y + z 1 {y > 3} {y > 3} x := y + 2 {x > 5} {y + z > 4} y := y + z 1; x := y + 2 {x > 5}
P P {P } S {Q } Q Q {P } S {Q} { } { } ((y > 4) (z > 1)) (y + z > 5) {y + z > 5} y := y + z {y > 5} (y > 5) (y > 3) {(y > 4) (z > 1)} y := y + z {y > 3}
{P B} S 1 {Q} {P B} S 2 {Q} {P } if B then S 1 else S 2 {Q} {(y > 4) (z > 1)} y := y + z {y > 3} {(y > 4) (z > 1)} y := y 1 {y > 3} {y > 4} if (z > 1) then y := y+z else y := y-1 {y > 3}
{I B} S {I} {I} while BS{I B}
{I B} S {I} {I} while BS{I B} {(y = x + z) (z = 0)} x := x + 1; z := z 1 {y = x + z} {y = x + z} while (z!= 0){x := x+1; z := z-1} {(y = x + z) (z = 0)} { } { } { {(y = x + z) true} x := x + 1; z := z 1 {y = x + z} {y = x + z} while (true){x := x+1; z := z-1} {(y = x + z) false}
i := 0; while i < 10 b := random_bool(); if b then i := i + 1; end 0 i 0 i 10 (0 i<10) (i = 10 b) The strongest invariant
{Q[E/x]} x := E {Q} {P } S 1 {R} {R} S 2 {Q} {P } S 1 ; S 2 {Q} } { P P {P } S {Q } Q Q {P } S {Q} { } { } {P B} S 1 {Q} {P B} S 2 {Q} {P } if B then S 1 else S 2 {Q} {I B} S {I} {I} while BS{I B}
int bar(int n) { local int k, int j; k := 0; j := 1; while (k!= n) { k := k + 1; j := 2 + j; } return(j); } {n 0} x = bar(n) {x =1+2n} { } { }
{n > 0} Precondition k := 0 {ϕ 1 } Midcondition j := 1 {ϕ 2 } Midcondition while (k!= n) { k := k+1; j := 2+j} {j =1+2.n} Postcondition {ϕ 2 } while (k!= n) { k := k+1; j := 2+j} {j =1+2.n}?
{ϕ 2 } while (k!= n) { k := k+1; j := 2+j} {j =1+2.n}? k =0 j =1 k =1 j =2+1 k =2 j =2+2+1...... { } { (j =1+2.k)
A Hoare logic proof To prove: {ϕ 2 } while (k!= n) k := k+1; j := 2+j {j =1+2.n} using loop invariant (j = 1 + 2.k) If we can show: ϕ 2 (j =1+2.k) {(j = 1 + 2.k) (k = n)} k := k+1; j:= 2+j {j = 1 + 2.k} ((j =1+2.k) (k = n)) (j =1+2.n) then By inference rule for loops {(j = 1 + 2.k) (k = n)} k := k+1; j:= 2+j {j = 1 + 2.k} {j = 1 + 2.k} while (k!= n) k := k+1; j:= 2+j {(j = 1 + 2.k) (k = n)} By inference rule for strengthening precedents and weakening consequents ϕ 2 (j =1+2.k) {j = 1 + 2.k} while (k!= n) k := k+1; j:= 2+j {(j = 1 + 2.k) (k = n)} ((j =1+2.k) (k = n)) (j =1+2.n) {ϕ 2 } while (k!= n) k := k+1; j:= 2+j {(j =1+2.n)}
How do we show: Note: ϕ 2 (j =1+2.k) {(j = 1 + 2.k) (k = n)} k := k+1; j:= 2+j {j = 1 + 2.k} ((j =1+2.k) (k = n)) (j =1+2.n) ϕ 2 (j =1+2.k) holds trivially if ϕ 2 is (j =1+2.k) ((j =1+2.k) (k = n)) (j =1+2.n) holds trivially in integer arithmetic Only remaining proof subgoal: {(j = 1 + 2.k) (k = n)} k := k+1; j:= 2+j {j = 1 + 2.k}
To show: {(j = 1 + 2.k) (k = n)} k := k+1; j:= 2+j {j = 1 + 2.k} Applying assignment rule twice {2+j =1+2.k} j := 2+j {j =1+2k} {2+j =1+2.(k + 1)} k := k+1 {2+j =1+2.k} Simplifying and applying sequential composition rule {1+j =2.k} j := 2+j {j =1+2k} {j =1+2.k)} k := k+1 {1+j =2.k} {j =1+2.k} k := k+1; j := 2+j {j =1+2.k} Applying rule for strengthening precedent (j =1+2.k) (k = n)} (j =1+2.k) {j =1+2.k} k := k+1; j := 2+j {j =1+2.k} {(j = 1 + 2.k) (k = n)} k := k+1; j := 2+j {j = 1 + 2.k}
We have thus shown that with ϕ 2 as (j =1+2.k) {ϕ 2 } while (k!= n) k := k+1; j := 2+j {j =1+2.n} is valid Recall our template: {n > 0} Precondition k := 0 {ϕ 1 } Midcondition j := 1 {ϕ 2 : j =1+2.k} Midcondition while (k!= n) k := k+1; j := 2+j {j =1+2.n} Postcondition The only missing link now is to show {n > 0} k := 0 {ϕ 1 } and {ϕ 1 } j := 1 {j =1+2.k}
To show {n > 0} k := 0 {ϕ 1 } and {ϕ 1 } j := 1 {j =1+2.k} Applying assignment rule twice and simplifying: {0 =k} j := 1 {j =1+2.k} {true} k := 0 {0 =k} Choose ϕ 1 as (k = 0), so {ϕ 1 } j := 1 {j =1+2.k} holds. Applying rule for strengthening precedent: (n > 0) true {true} k := 0 {ϕ 1 : k =0} {n > 0} k := 0 {ϕ 1 : k =0}