% @(#)$Id: PointerWithNull.lsl,v 1.9 1995/07/26 15:43:24 leavens Exp $
% Pointers, with the possibility of the null pointer and invalid pointers.

PointerWithNull(Elem): trait
  includes PrePointer(Elem)

  introduces
    NULL: -> Ptr[Elem]
    isNull, notNull, isLegal, isValid: Ptr[Elem] -> Bool
    allocated, allAllocated: Ptr[Elem] -> Bool
    minIndex, maxIndex: Ptr[Elem] -> int
    legalIndex, validUpTo, allocated, allocatedUpTo: Ptr[Elem], int -> Bool
    validInRange, allocatedInRange: Ptr[Elem], int, int -> Bool
    * __: Ptr[Elem] -> Elem
    __[__]: Ptr[Elem], int -> Elem
    slice: Ptr[Elem], int, int -> Arr[Elem]

  asserts
    sort Ptr[Elem] generated by NULL, [__,__]
    sort Ptr[Elem] partitioned by isNull, .idx, .locs
    \forall p: Ptr[Elem], i,j,siz: int
       isNull(p) == (p = NULL);
       notNull(p) == ~(p = NULL);
       legalIndex(p,i) == if isNull(p) then false
                          else ((minIndex(p) <= i) /\ (i <= maxIndex(p)));
       isLegal(p) == isNull(p) \/ allocated(p.locs, p.idx);
       isValid(p) == notNull(p) /\ allocated(p.locs, p.idx);
       allocated(p) == isValid(p);
       allocated(p,i) == allocated(p+i);
       allAllocated(p) == isValid(p) /\ allAllocated(p.locs);
       validInRange(p,i,j) == if i > j then true
                              else isValid(p+i) /\ validInRange(p,i+1,j);
       validUpTo(p,siz) == validInRange(p, 0, siz-1);
       allocatedInRange(p, i, j) == validInRange(p,i,j);
       allocatedUpTo(p,siz) == allocatedInRange(p, 0, siz-1);

       notNull(p) => (minIndex(p) = -(p.idx));
       notNull(p) => (maxIndex(p) = maxIndex(p.locs) - p.idx);
       allocated(p) => (*p = p.locs[p.idx]);
       allocated(p,i) => (p[i] = p.locs[p.idx + i]);

       notNull(p) => (slice(p, i, j) = slice(p.locs, p.idx+i, p.idx+j));

  implies \forall p: Ptr[Elem], i: int
      notNull(p) => (minIndex(p) + maxIndex(p) = maxIndex(p.locs));
      isValid(p) == notNull(p) /\ isLegal(p);
      allocated(p,i) => (p[i] = *(p + i));
      allocated(p,i) => (p[i] = (locs(p))[p.idx + i]);
      isValid(p) => isLegal(p);
      allocated(p) => isLegal(p);
    converts .idx, .locs, locs, index, isNull, notNull, isLegal, isValid,
             allocated: Ptr[Elem] -> Bool, allAllocated: Ptr[Elem] -> Bool,
             minIndex: Ptr[Elem] -> int, maxIndex: Ptr[Elem] -> int,
             legalIndex: Ptr[Elem], int -> Bool,
             allocated: Ptr[Elem], int -> Bool,
             validUpTo, allocatedUpTo: Ptr[Elem], int -> Bool,
             validInRange, allocatedInRange: Ptr[Elem], int, int -> Bool,
             slice: Ptr[Elem], int, int -> Arr[Elem]
     exempting \forall i,j: int
               NULL.idx, NULL.locs, locs(NULL),
               index(NULL), minIndex(NULL), maxIndex(NULL), slice(NULL, i, j)

[Index]

HTML generated using lcpp2html.