% @(#) $Id: Entry_Pre_Trait.lsl,v 1.1 1998/08/27 15:11:53 leavens Exp $

Entry_Pre_Trait(Entry, Loc, Val): trait

  assumes char, Pointer(Obj, char), int,
          TypedObj(Loc, Ptr[Obj[char]]), TypedObj(Loc, int),
          contained_objects(Loc[Ptr[Obj[char]]]), contained_objects(Loc[int])

  includes NoContainedObjects(Val), contained_objects(Entry)

  Entry tuple of sym: Loc[Ptr[Obj[char]]], val: Loc[int]
  Val tuple of sym: Ptr[Obj[char]], val: int

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

  asserts
    \forall entry: Entry, opoc: Loc[Ptr[Obj[char]]], oi: Loc[int], st: State
       contained_objects([opoc,oi], st)
         == {asTypeTaggedObject(opoc)} \U {asTypeTaggedObject(oi)};
       eval(entry,st) == [eval(entry.sym, st), eval(entry.val, st)];
       allocated(entry,st)
         == allocated(entry.sym, st) /\ allocated(entry.val, st);
       assigned(entry,st)
         == assigned(entry.sym, st) /\ assigned(entry.val, st);

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

[Index]

HTML generated using lcpp2html.