% @(#)$Id: TopLevelAliased.lsl,v 1.8 1995/11/06 07:19:07 leavens Exp $
TopLevelAliased(Loc, T) : trait
   includes TypedObj
   assumes contained_objects(T)
   introduces
      top_level_aliased: T, T, State -> Bool
      top_level_aliased: Loc[T], Loc[T], State -> Bool
   asserts \forall l1, l2: Loc[T], v1,v2: T, st: State
      top_level_aliased(v1, v2, st)
        == not((ignoringTypeTags(contained_objects(v1,st))
                \I ignoringTypeTags(contained_objects(v2,st)))
               = {});
      top_level_aliased(l1, l2, st)
        == (l1 = l2) \/ top_level_aliased(eval(l1,st), eval(l2,st), st);

[Index]

HTML generated using lcpp2html.