% @(#)$Id: PointerToArray.lsl,v 1.14 1995/12/24 23:53:25 leavens Exp $
% Pointers to arrays, as opposed to pointers to single objects (within arrays)

PointerToArray(SubObjArr, SubValArr): trait

  includes MultiDimensionalArray(SubObjArr, SubValArr),
           PointerWithNull(SubObjArr),
           PointerAllocatedAuxFuns(Ptr[SubObjArr]),
           PointerAssignedAuxFuns(Ptr[SubObjArr]),
           contained_objects(Ptr[SubObjArr])

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

  asserts
    \forall p: Ptr[SubObjArr], i,j,siz: int, st: State
      allocated(p, i, st) == allocated(p,i) /\ allAllocated(*(p+i), st);
      assigned(p, i, st) == allocated(p,i) /\ allAssigned(*(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 {}
           else objectsInRange(p.locs, p.idx + i, p.idx + j);
      objectsUpTo(p, siz) == objectsInRange(p, 0, siz-1);

  implies
    \forall st: State
      contained_objects(NULL, st) == {};

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

[Index]

HTML generated using lcpp2html.