% @(#)$Id: Invariant_Visible.lsl,v 1.1 1997/01/27 20:33:15 leavens Exp $
Invariant_Visible(Loc,T): trait
  includes TypedObj(Loc, T)
  assumes visible, i_pred(Loc,T)
  asserts
    \forall o: Loc[T], st: State
      (assigned(o,st) /\ visible(st)) => invariant_pred(o,st);

[Index]

HTML generated using lcpp2html.