% @(#)$Id: Pointer.lsl,v 1.35 1995/12/24 02:51:14 leavens Exp $
% Pointers to single objects (perhaps within an array, but not to arrays)

Pointer(Loc, Val): trait

  includes Array(Loc, Val), PointerWithNull(Loc[Val]),
           PointerAllocatedAuxFuns(Ptr[Loc[Val]]),
           PointerAssignedAuxFuns(Ptr[Loc[Val]]),
           contained_objects(Ptr[Loc[Val]])

  assumes TypedObj(Loc, Val)

  introduces
    allocated, assigned: Ptr[Loc[Val]], int, State -> Bool
    isLegal, isValid, nullOrAssigned: Ptr[Loc[Val]], State -> Bool
    eval: Ptr[Loc[Val]], State -> Arr[Val]
    objectsInRange: Ptr[Loc[Val]], int, int -> Set[TypeTaggedObject]
    objectsUpTo: Ptr[Loc[Val]], int -> Set[TypeTaggedObject]

  asserts
    \forall p: Ptr[Loc[Val]], i,j,siz: int, st: State
      allocated(p, i, st) == allocated(p, i) /\ allocated(*(p+i), st);
      assigned(p, i, st) == allocated(p, i) /\ assigned(*(p+i), st);
      isLegal(p, st) == isNull(p) \/ allocated(p, st);
      isValid(p, st) == allocated(p, st);
      nullOrAssigned(p, st) == isNull(p) \/ assigned(p, st);
      eval(p,st) == if isValid(p) then eval(p.locs,st) else create(0);
      contained_objects(p, st)
        == if ~isValid(p) then {}
           else contained_objects(p.locs, st);
      objectsInRange(p, i, j)
        == if isValid(p) then objectsInRange(p.locs, p.idx + i, p.idx + j)
           else {};
      objectsUpTo(p, siz) == objectsInRange(p, 0, siz-1);

  implies
    \forall p: Ptr[Loc[Val]], i:int, st: State
      assigned(p, st) => allocated(p, st);
      allocated(p, st) => notNull(p) /\ isLegal(p, st);
      contained_objects(NULL, st) == {};
      size(contained_objects(p, st)) <= (maxIndex(p.locs) + 1);

   converts
      allocated: Ptr[Loc[Val]], int, State -> Bool,
      assigned: Ptr[Loc[Val]], int, State -> Bool,
      isLegal: Ptr[Loc[Val]], State -> Bool,
      isValid: Ptr[Loc[Val]], State -> Bool,
      nullOrAssigned: Ptr[Loc[Val]], State -> Bool,
      eval: Ptr[Loc[Val]], State -> Arr[Val],
      contained_objects: Ptr[Loc[Val]], State -> Set[TypeTaggedObject],
      objectsInRange: Ptr[Loc[Val]], int, int -> Set[TypeTaggedObject],
      objectsUpTo: Ptr[Loc[Val]], int -> Set[TypeTaggedObject]
     exempting
       \forall p: Ptr[Loc[Val]]
         eval(p,bottom), eval(p,emptyState)

[Index]

HTML generated using lcpp2html.