I need to develop a program with the following specification:
$$\{Q: x= A \wedge y=B\}\ ord2\ \{R: x\leqslant y \wedge [(x=A\wedge y=B)\vee(x=B \wedge y=A)]\}$$
Solution:
What I understand is to develop a program which sorts the both input values -$x$ and $y$- such as $x$ is always less than or equal to $y$ at the end of the program (post-condition $Q$).
This is my first attempt (it's written in GCL):
$[\text{Ctx}\ C: x,y\in \mathrm{Z}$
$\{Q: x= A \wedge y=B\}$
$if\ x > y \rightarrow $
$\ \ \ \ temp := x;$
$\ \ \ \ x := y;$
$\ \ \ \ y := temp;$
$else $
$\ \ \ \ skip;$
$\{R: x\leqslant y \wedge [(x=A\wedge y=B)\vee(x=B \wedge y=A)]\}$
$]$
Is it correct?