// @(#)$Id: add_one_desugared.lh,v 1.5 1997/06/03 20:29:56 leavens Exp $
extern void add_one(int& x) throw();
//@ behavior {
//@   requires allocated(x, pre)   // added by the syntactic sugar
//@            /\ assigned(x, pre) // x is allocated and has a value
//@            /\ x^ < INT_MAX;    // x^ : pre-value of x
//@   modifies x;                  // x  : an object
//@   ensures x' = x^ + 1;         // x' : post-value of x
//@ }

[Index]

HTML generated using lcpp2html.