use axiomatic semantics to prove that the following code to swap two integer variables is correct.

Do this by finding the assertions labeled P1 and P2 (weakest pre-condition)

{Precondition: x = x0 and y = y0}

x := x + y;

{P1}

y := x - y;

{P2}

x := x - y;

{Postcondition: x = y0 and y = x0}