// @(#)$Id: make_zero_or_one.lh,v 1.7 1997/06/03 20:30:14 leavens Exp $
extern void make_zero_or_one(const int* x) throw();
//@ behavior {
//@ requires assigned(x, pre);
//@ modifies *x; // error!
//@ ensures (*x)' = (*x)^ \mod 2;
//@ }
[Index]
HTML generated using lcpp2html.