% @(#) $Id: listelem_Pre_Trait.lsl,v 1.1 1997/07/31 17:26:39 leavens Exp $

% This trait would be automatically constructed by Larch/C++
% as part of the model of the members in the listelem class.

listelem_Pre_Trait(listelem, Loc, Val): trait

  assumes int, Pointer(Obj, listelem), MutableObj(listelem),
          cpp_member_function,
          TypedObj(Loc, Ptr[Obj[listelem]]), TypedObj(Loc, int),
          ConstObj(cpp_member_function),
          contained_objects(Loc[Ptr[Obj[listelem]]]),
          contained_objects(Loc[int])

  includes NoContainedObjects(Val), contained_objects(listelem)

  listelem tuple of car: Loc[int], cdr: Loc[Ptr[Obj[listelem]]],
                    get_value: ConstObj[cpp_member_function],
                    get_next: ConstObj[cpp_member_function],
                    set_value: ConstObj[cpp_member_function],
                    set_next: ConstObj[cpp_member_function]

  Val tuple of car: int, cdr: Ptr[Obj[listelem]] ,
                    get_value: cpp_member_function,
                    get_next: cpp_member_function,
                    set_value: cpp_member_function,
                    set_next: cpp_member_function

  introduces
    eval: listelem, State -> Val
    allocated, assigned: listelem, State -> Bool

  asserts
    \forall le: listelem, oi: Loc[int], op: Loc[Ptr[Obj[listelem]]],
            gv,gn,sv,sn: ConstObj[cpp_member_function], st: State
       contained_objects([oi,op,gv,gn,sv,sn], st)
         == {asTypeTaggedObject(oi)} \U {asTypeTaggedObject(op)}
            \U {asTypeTaggedObject(gv)} \U {asTypeTaggedObject(gn)}
            \U {asTypeTaggedObject(sv)} \U {asTypeTaggedObject(sn)};

       eval(le, st)
         == [eval(le.car,st), eval(le.cdr,st),
             eval(le.get_value,st), eval(le.get_next,st),
             eval(le.set_value,st), eval(le.set_next,st)];

       allocated(le, st)
         == allocated(le.car, st) /\ allocated(le.cdr, st)
          /\ allocated(le.get_value, st) /\ allocated(le.get_next, st)
          /\ allocated(le.set_value, st) /\ allocated(le.set_next, st);

       assigned(le,st)
         == assigned(le.car, st) /\ assigned(le.cdr, st)
          /\ assigned(le.get_value, st) /\ assigned(le.get_next, st)
          /\ assigned(le.set_value, st) /\ assigned(le.set_next, st);

  implies
    converts
      contained_objects: listelem, State -> Set[TypeTaggedObject],
      eval: listelem, State -> Val,
      allocated: listelem, State -> Bool, assigned: listelem, State -> Bool

[Index]

HTML generated using lcpp2html.