// @(#)$Id: inc_counter.lh,v 1.8 1997/06/03 20:30:07 leavens Exp $
extern int inc_counter(void) throw();
//@ behavior {
//@   extern int counter;
//@   requires assigned(counter, pre) /\ counter^ < INT_MAX;
//@   modifies counter;
//@   ensures counter' = counter + 1;
//@ }

[Index]

HTML generated using lcpp2html.