The Hoare Triple law for the assignment command says
| {P} x:=E {Q} ≡ [P ⟹ Q(x := E) ∧ def.E] |
Example: Prove {P1 ∧ P2} x, y := x*x, y div 2 {P1}, where
The idea expressed by this Hoare Triple is that execution of the assignment statement, which (possibly) modifies the values of both x and y, should leave the value of xy unchanged. (Note that C is a ghost (aka rigid) variable whose purpose is to be able to refer to the "initial" value of xy in the postcondition.) Note that div denotes integer division, so that
| y div 2 = { | y/2 | if even.y |
| (y−1)/2 | if ¬even.y ∧ y>0 | |
| (y+1)/2 | if ¬even.y ∧ y<0 |
Solution: By the Hoare Triple law for assignment, it suffices to prove P1 ∧ P2 ⟹ P1(x,y := x*x, y div 2). (We assume that both x and y are well-defined, so that the expressions x*x and y div 2 are, too.) The usual approach is to assume the antecedant and to show the consequent:
Assume P1 ∧ P2
P1(x,y := x*x, y div 2)
= < defn of P1 and textual substitution >
C = (x*x)y div 2
= < algebra: x*x = x2 >
C = (x2)y div 2
= < algebra: (ab)c = abc >
C = x2(y div 2)
= < y div 2 = y/2 follows from assumption P2 (i.e., even.y) >
C = x2(y/2)
= < algebra: a(b/a) = b (for a ≠ 0) >
C = xy
= < assumption P1 >
true
|
Now suppose that we use the wp approach instead of the Hoare Triple approach. The relationship between wp and Hoare Triples is
| {P} S {Q} ≡ [P ⇒ wp.S.Q] |
Furthermore, the wp assignment rule is
| [wp.(x:=E).Q ≡ (Q(x:=E) ∧ def.E)] |
Hence, to prove {P1 ∧ P2} x,y := x*x, y div 2 {P1} we show the equivalent
The usual approach is to assume the antecedant and to show the consequent:
Assume P1 ∧ P2.
wp.(x,y := x*x, y div 2).P1
= < wp assignment rule >
P1(x,y := x*x, y div 2)
= ... continue as in proof above
|