% @(#)$Id: PersonInvariant.lsl,v 1.2 1997/07/30 22:07:40 leavens Exp $
PersonInvariant(Loc): trait
  includes i_pred(Loc,Person), Person_Trait
  asserts
    \forall self: Loc[Person], any: State
      invariant_pred(self, any)
        == len(eval(eval(self,any).name, any)) > 0
           /\ eval(eval(self,any).age, any) >= 0;

[Index]

HTML generated using lcpp2html.