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.