// @(#)$Id: inc4.lh,v 1.4 1999/03/04 23:15:33 leavens Exp $

#include "Overflow.lh"

extern void inc4(int& i) throw(Overflow*);
//@ behavior program {
//@   requires assigned(i, pre);
//@   if (i + 4 <= INT_MAX) {
//@      i += 4;
//@   } else {
//@     assert i^ + 4 > INT_MAX;
//@     throw new Overflow();
//@   }
//@ }

[Index]

HTML generated using lcpp2html.