SE 504
Proving Correctness of an Assignment (2)

The Hoare Triple law for the assignment command says

{P} x:=E {Q}   ≡   [P  ⟹  Q(x := E) ∧ def.E]

In most cases, we assume that the expression(s) E is(are) well-defined, so we ignore the def.E term.

Example: Prove {P} z,y := z*x,y+1 {P}, where P: z = xy ∧ y≥0

Solution: By the Hoare Triple law for assignment, it suffices to prove P ⟹ P(z,y := z*x,y+1). (We assume that variables z and y are well-defined and thus so are the expressions z*x and y+1.) The usual approach is to assume the antecedant and to show the consequent:

Assume P. 
     P(z,y := z*x,y+1)

  =     < defn of P >

     (z = xy ∧ y≥0)(z,y := z*x,y+1)

  =     < textual substitution >

     z*x = xy+1 ∧ y+1 ≥ 0

  =     < y+1 ≥ 0 follows from assumption y≥0 >

     z*x = xy+1 ∧ true

  =     < (3.39) true is identity of ∧ >

     z*x = xy+1 

  =     < Assumption z = xy >

     xy*x = xy+1

  =     < algebra: ab * ac = ab+c >

     xy+1 = xy+1

  =     < = is reflexive >

     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 law is

[wp.(x:=E).Q   ≡   Q(x:=E) ∧ def.E]

Hence, to prove {P} z,y := z*x,y+1 {P} we show the equivalent

[P  ⟹  wp.(z,y := z*x,y+1).P]

(Once again we've assumed that the variables are well-defined.) The usual approach is to assume the antecedant and to show the consequent:

Assume P. 
     wp.(z,y := z*x,y+1).P

  =     < wp assignment rule >

     P(z,y := z*x,y+1)

  =     ... continue as in proof above