// @(#) $Id: set_ref_to_one.lh,v 1.5 1997/06/03 20:30:20 leavens Exp $
extern void set_to_one(int &i) throw();
//@ behavior {
//@   modifies i;
//@   ensures assigned(i, post) /\ i' = 1;
//@ }

[Index]

HTML generated using lcpp2html.