Let us now investigate the reasons what made the earlier tricky exchange program work. In order to do that we formulate the same program structure using abstract terms p,q,r :
{ x = A and y = B }
x := p(x,y)
y := q(x,y)
x := r(x,y)
{ x = B and y = A }
NPPV generates the following verification condition :
q(p(A,B),B) = A
r(p(A,B),A) = B
On close inspection we find that these are precisely the defining equations
of a quasigroup. To emphasize this, let us replace p, q and r with infix symbols
. We see that the equations specify that * should be a binary
operation which is both left- and right-cancellative, i.e.
(A * B) / B = A
A \ (A * B) = B.
Thus we find that the content of two variables can be switched by a sequence of three assignments, iff the underlying data structure contains a quasiqroup operation.