Slide 11.6: Example I of program correctness
Slide 11.8: Example II of program correctness
Home

Example I of Program Correctness (Cont.) 

{x = X and y = Y}  t := x; x := y; y := t;  {x = Y and y = X}
We first compute wp(C, Q) as follows: 
  wp(t:=x; x:=y; y:=t, x=Y and y=X)
= wp(t:=x, wp(x:=y; y:=t, x=Y and y=X))     (Statement-lists)
= wp(t:=x, wp(x:=y, wp(y:=t, x=Y and y=X))) (Statement-lists)
= wp(t:=x, wp(x:=y, wp(y:=t, x=Y) and
                    wp(y:=t, y=X)))         (Conjunction)
= wp(t:=x, wp(x:=y, wp(y:=t, x=Y)) and
           wp(x:=y, wp(y:=t, y=X)))         (Conjunction)
= wp(t:=x, wp(x:=y, wp(y:=t, x=Y))) and
  wp(t:=x, wp(x:=y, wp(y:=t, y=X)))         (Conjunction)
by distributivity of conjunction and the axiomatic semantics of statement-lists. Now 
  wp(t:=x, wp(x:=y, wp(y:=t, x=Y)))
= wp(t:=x, wp(x:=y, x=Y))                   (Assignment)
= wp(t:=x, y=Y)                             (Assignment)
= (y = Y)                                   (Assignment)
and 
  wp(t:=x, wp(x:=y, wp(y:=t, y=X)))
= wp(t:=x, wp(x:=y, t=X))                   (Assignment)
= wp(t:=x, t=X)                             (Assignment)
= (x = X)                                   (Assignment)
by the rule of substitution for assignments. Thus, 
  wp(t:=x; x:=y; y:=t, x=Y and y=X)
= (x = X and y = Y)
The second step is to show that P → wp(C, Q). But in this case P actually equals the weakest precondition, since P = (x=X and y=Y). Since P = wp(C, Q), clearly P → wp(C, Q). The proof of correctness is complete.