Refinement in B (an example)

MACHINE
swap
VARIABLES
xx, yy
INVARIANT
xx : NAT & yy : NAT
INITIALISATION
xx :: NAT ||
yy :: NAT
OPERATIONS
echange =
BEGIN
xx := yy ||
yy := xx
END
END

REFINEMENT
swapR
REFINES
swap
VARIABLES
xr, yr, zr
INVARIANT
xr= xx & yr = yy & zr : NAT
INITIALISATION
xr, yr, zr:= 0, 0, 0
OPERATIONS
echange =
BEGIN
zr := xr;
xr := yr;
yr := zr
END
END


Type check and proofs OK with Atelier B