// @(#)$Id: swap-desugared.lh,v 1.5 1997/06/03 20:30:21 leavens Exp $
extern void swap(int& x, int& y) throw();
//@ behavior {
//@   requires allocated(x, pre) /\ allocated(y, pre);
//@   modifies x, y;
//@   ensures ((x!post) = (y!pre)) /\ ((y!post) = (x!pre));
//@ }

[Index]

HTML generated using lcpp2html.