% @(#)$Id: ToListTrait.lsl,v 1.8 1997/07/25 16:36:57 leavens Exp $

ToListTrait: trait
  assumes MutableObj(listelem), Pointer(Obj, listelem)  % Larch/C++ traits
  includes listelem_Trait, List(int, List[int], int for Int),
           Set(Obj[listelem], Set[Obj[listelem]], int for Int)
  introduces
    circular: Ptr[Obj[listelem]], State -> Bool
    circular2: Ptr[Obj[listelem]], State, Set[Obj[listelem]] -> Bool
    toList: Ptr[Obj[listelem]], State -> List[int]
    last_elem: Ptr[Obj[listelem]], State -> Obj[listelem]
    list_objs: Ptr[Obj[listelem]], State -> Set[Object]
    list_objs2: Ptr[Obj[listelem]], State, Set[Object] -> Set[Object]
    top_level_aliased: Ptr[Obj[listelem]], Ptr[Obj[listelem]], State -> Bool
  asserts
   \forall i: int, p, p1, p2: Ptr[Obj[listelem]], st: State,
                  soe: Set[Obj[listelem]], so: Set[Object]
      isLegal(p) =>
	(circular(p,st) = circular2(p, st, {}));
      isLegal(p) =>
	(circular2(p, st, soe) =
		   (notNull(p)
			/\ (((*p) \in soe)
                            \/ circular2(eval(eval(*p, st).cdr, st),
                                         st, soe \U {*p}))));
      (isLegal(p) /\ not(circular(p, st)))
	=> (toList(p, st) =
		(if isNull(p) then empty
		 else {eval(eval(*p, st).car, st)}
                      || toList(eval(eval(*p, st).cdr, st), st)));
      (isValid(p) /\ not(circular(p, st)))
	=> (last_elem(p, st) = (if isNull(eval(eval(*p, st).cdr, st))
                                then *p
				else last_elem(eval(eval(*p, st).cdr, st),
                                               st)));
      isLegal(p)
	=> (list_objs(p, st) = list_objs2(p, st, {}));
      isLegal(p)
	=> (list_objs2(p, st, so) =
		   (if isNull(p) \/ (widen(*p) \in so)
		    then so
		    else list_objs2(eval(eval(*p, st).cdr, st),
                                    st, so \U {widen(*p)})));
      (isLegal(p1) /\ isLegal(p2))
	=> (top_level_aliased(p1, p2, st) =
		not(list_objs(p1, st) \I list_objs(p2, st) = {}));
   implies
     \forall i: int, p: Ptr[Obj[listelem]], st: State
       (isLegal(p) /\ not(circular(p, st)))
	=> (list_objs(p, st) = (if isNull(p)
                                then {}
				else {widen(*p)}
				     \U list_objs(eval(eval(*p, st).cdr, st),
                                                  st)));

[Index]

HTML generated using lcpp2html.