% @(#)$Id: PersonSetTrait.lsl,v 1.12 1997/07/31 02:43:26 leavens Exp $
PersonSetTrait: trait
  includes Person_Trait, MutableObj(Person),
           Set(Person, Set[Person]),
           Set(Obj[Person], Set[Obj[Person]]),
           contained_objects(Set[Obj[Person]])
  introduces
    eval: Set[Obj[Person]], State -> Set[Person]
    allocated, assigned: Set[Obj[Person]], State -> Bool

  asserts
   \forall pv: Person, p: Obj[Person], s: Set[Obj[Person]], st: State
      asTypeTaggedObject(p) \in contained_objects(s, st) == p \in s;
      pv \in eval(s, st) == \E p (p \in s /\ eval(p, st) = pv);
      allocated(s, st);
      assigned(s, st);

[Index]

HTML generated using lcpp2html.