// @(#)$Id: add_one.lh,v 1.6 1997/06/03 20:29:55 leavens Exp $
extern void add_one(int& x) throw();
//@ behavior {
//@   requires 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.