{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.