% @(#)$Id: container_objs.lsl,v 1.8 1995/08/24 17:31:16 leavens Exp $
% This trait is useful for defining contained_objects for generic containers,
% such as Set<T>, List<T>, etc.

container_objs(E,C): trait
  includes contained_objects(C) % introduces the signature
  assumes Container(E,C), contained_objects(E)
  asserts
    \forall e: E, c: C, st: State, o: Object
      contained_objects(c, st)
        == if isEmpty(c) then {}
           else contained_objects(head(c), st)
                \U contained_objects(tail(c), st)
  implies
    with_member_objs(E,C)
    converts contained_objects: C, State -> Set[TypeTaggedObject]

[Index]

HTML generated using lcpp2html.