// @(#)$Id: bad_myo.lh,v 1.4 1998/08/27 22:56:48 leavens Exp $

#include "Person.lh"

void Person::Make_Year_Older() throw();
//@ behavior {
//@   requires redundantly assigned(age,pre) /\ visible(pre) /\ age^ >= 0;
//@   modifies age;
//@   ensures age' = -3;   // wrong!
//@   ensures redundantly assigned(age,post) /\ visible(post) /\ age' >= 0;
//@ }

[Index]

HTML generated using lcpp2html.