// @(#)$Id: inc3.lh,v 1.11 1999/03/04 23:16:10 leavens Exp $

#include "Overflow.lh"

extern void inc3(int& i) throw(Overflow*);
//@ behavior {
//@   requires assigned(i, pre);
//@   modifies i;
//@   ensures (returns /\ i' = i^ + 3)
//@           \/ (throws(Overflow*) /\ unchanged(i));
//@   example i^ = 4 /\ i' = 7 /\ returns;
//@   example i^ = 4 /\ i' = 4 /\ throws(Overflow*);
//@ }

[Index]

HTML generated using lcpp2html.