Go to the first, previous, next, last section, table of contents.


11.8 Pointer Types

The Larch/C++ model of C++ pointers is based on a simple idea, to which a model of the 0 pointer is added.

The simple idea is that a non-null pointer is an offset into a sequence of one or more adjacent objects. Thus, most pointers, excepting the 0 pointer, have an abstract value that is an index into an array, with two bounding indexes. The following trait describes this idea, and follows ideas in LCL (see Chapter 5 of [Guttag-Horning93]). The idea is that a pointer is modeled as a tuple of an index and an array. (The array may just have one element for a pointer to a variable.) The pointer is thus pointing at the indexed element of the array.

% @(#)$Id: PrePointer.lsl,v 1.7 1995/06/20 22:49:38 leavens Exp $
% Model of pointers as index into an array.
% This follows the idea in LCL [page 60, Guttag-Horning93].

PrePointer(Elem): trait

  assumes Val_Array(Elem), int

  % This would be
  %   "Ptr[Elem] tuple of idx: int, locs: Arr[Elem]"
  % but don't want set_locs, "generated by" and "partitioned by" clauses

  introduces
    [__, __] : int, Arr[Elem] -> Ptr[Elem]
    &__ : Elem -> Ptr[Elem]                  % use if not in an array
    address_of : Arr[Elem], int -> Ptr[Elem] % use if in an array
    __.idx: Ptr[Elem] -> int
    __.locs: Ptr[Elem] -> Arr[Elem]
    locs: Ptr[Elem] -> Arr[Elem]
    index: Ptr[Elem] -> int
    set_idx: Ptr[Elem], int -> Ptr[Elem]
    __ + __: Ptr[Elem], int -> Ptr[Elem]
    __ - __: Ptr[Elem], int -> Ptr[Elem]
    __<__, __<=__, __>=__, __>__: Ptr[Elem], Ptr[Elem] -> Bool

  asserts \forall p: Ptr[Elem], i,j: int, a,a1: Arr[Elem],
                  st: State, l: Elem
    &l == [0,assign(create(1), 0, l)];
    address_of(a,i) == [i,a];
    ([i,a] = [j,a1]) == (i = j) /\ (a = a1);
    ([i,a]).idx == i;
    ([i,a]).locs == a;
    locs(p) == p.locs;
    index(p) == p.idx;
    set_idx([i,a], j) == [j,a];
    p + i == set_idx(p, p.idx + i);
    p - i == set_idx(p, p.idx - i);
    ([i,a] < [j,a]) == (i < j);
    ([i,a] > [j,a]) == (i > j);
    ([i,a] <= [j,a]) == (i <= j);
    ([i,a] >= [j,a]) == (i >= j);

  implies IsPO(<=, Ptr[Elem]), IsPO(>=, Ptr[Elem])

In C++, a pointer can be either pointing to something, or it can be a 0 pointer. The following trait, PointerWithNull, adds to the pointers modeled by PrePointer, the NULL pointer, which is the abstract value of the 0 pointer in C++. (The use of 0 as a pointer as well as an integer makes overloading resolution in a term difficult. The name chosen, NULL, should be fairly intuitive.)

% @(#)$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)

The symbol * is one way to dereference a valid pointer. Thus *p produces the object that p is currently pointing to. Another way to achieve a similar effect is to use subscripts; for example, p[0] and *p mean the same thing, as do *(p + i) and p[i], for an int i. The trait functions minIndex(p) and maxIndex(p) respectively denote the maximum number of objects before and after *p. The concept of a valid pointer is captured by the trait function isValid.

The trait functions attempt to make pointers act like array names, as is the case in C++. That is, with a pointer, p, one can write expressions such as p[i], or the equivalent *(p + i), if i is between minIndex(p) and maxIndex(p). Also, the trait functions legalIndex, validRange, and validUpTo can be used to describe the legal indexes into the array into which the pointer points. These are particularly useful, therefore, for arrays passed as parameters.

However, there are some differences between array names and pointers. A notational difference is that, with an array name, a, one can only use the form a[i], not *(a + i), in Larch/C++. Besides this notational distinction, another difference from C++ is that in Larch/C++ the notation a[i] is not defined for negative numbers i. A more profound difference is that an array name (a value of a sort such as Arr[Obj[T]]) cannot be null or invalid, whereas a pointer can be null or invalid.

The trait PointerWithNull is included by the traits Pointer and PointerToArray below. The first defines pointers to objects, and the second defines pointers to arrays. The main purpose of both is to define the trait functions eval, contained_objects, and others that are used for syntactic shorthands and for describing the objects pointed at by a pointer.

% @(#)$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)

The trait Pointer also includes the trait PointerAllocatedAuxFuns to define various predicates to test whether objects are allocated.

% @(#)$Id: PointerAllocatedAuxFuns.lsl,v 1.2 1995/07/26 04:26:19 leavens Exp $

PointerAllocatedAuxFuns(PtrT): trait
  assumes PointerAllocAuxSig(PtrT)
  includes ArrayAllocatedAuxFuns(PtrT)
  introduces
    allocated: PtrT, State -> Bool
  asserts
    \forall p: PtrT, st: State
      allocated(p, st) == allocated(p, 0, st);
  implies
   converts
      allocated: PtrT, State -> Bool

Some assumptions used by the trait PointerAllocatedAuxFuns are recorded in the trait PointerAllocAuxSig.

% @(#)$Id: PointerAllocAuxSig.lsl,v 1.2 1995/07/26 04:26:19 leavens Exp $

PointerAllocAuxSig(PtrT): trait
  includes ArrayAllocAuxSig(PtrT)
  introduces
    __+__: PtrT, int -> PtrT

The trait Pointer also includes the trait PointerAssignedAuxFuns to define various predicates to test whether objects are assigned.

% @(#)$Id: PointerAssignedAuxFuns.lsl,v 1.2 1995/07/26 04:26:19 leavens Exp $

PointerAssignedAuxFuns(PtrT): trait
  includes PointerAllocatedAuxFuns(PtrT,
        assigned for allocated: PtrT, State -> Bool,
        assigned for allocated: PtrT, int, State -> Bool,
        assignedUpTo for allocatedUpTo,
        allAssigned for allAllocated,
        assignedInRange for allocatedInRange)

The following trait is similar to the Pointer trait, but is used for pointers to arrays or multidimensional arrays.

% @(#)$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)

For a pointer to a member (declared using the ::* operator), the following trait is used. It is just like the trait for Pointer, except it uses sorts of the form PtrMbr[Obj[T]] instead of Ptr[Obj[T]].

% @(#)$Id: PointerToMember.lsl,v 1.1 1995/12/23 03:06:03 leavens Exp $
% Pointers to members that are single objects
% (perhaps within an array, but not to arrays)
PointerToMember(Loc, Val): trait
  includes Pointer(Loc, Val, PtrMbr for Ptr)

For pointers to members that are arrays, the following trait is used.

% @(#)$Id: PointerToMemberArray.lsl,v 1.1 1995/12/23 03:07:28 leavens Exp $
% Pointers to members that are single objects
% (perhaps within an array, but not to arrays)
PointerToMemberArray(Loc, Val): trait
  includes PointerToArray(Loc, Val, PtrMbr for Ptr)

When a pointer type is used in a Larch/C++ specification, an instantiation of one or more of the traits above is automatically used in the specification. For example, when a type such as the one in the following typedef

typedef T *tpointer;

or the equivalent formal parameter type T [], is mentioned in a Larch/C++ specification, the trait Pointer(Obj, T) will be implicitly used in the interface specification module in which it appears. This also applies to declarations of global variables and formal parameters, as shown in the following table.

Declaration         Used Traits (not counting MutableObj and ConstObj)
-----------         ------------------------------------------------------
int *ip;            Pointer(Obj, int)
int ip[];           Pointer(Obj, int)
const int *ip;      Pointer(ConstObj, int)
const int ip[];     Pointer(ConstObj, int)
int *const ip;      Pointer(Obj, int)
int ** ip;          Pointer(Obj, Ptr[Obj[int]]),  Pointer(Obj, int)
int *x[10];         Array(Obj, Ptr[Obj[int]]),    Pointer(Obj, int)
int *const x[10];   Array(ConstObj, Ptr[Obj[int]])
                    Pointer(Obj, int)
int (*x)[10];       PointerToArray(Arr[Obj[int]], Arr[int]),
                    Array(Obj, int)
const int x[][10];  PointerToArray(Arr[ConstObj[int]], Arr[int]),
                    Array(ConstObj, int)
int (*x)[10][20];   PointerToArray(Arr[Arr[Obj[int]]], Arr[Arr[int]]),
                    Array(Obj, int),
                    MultiDimensionalArray(Arr[Obj[int]], Arr[int]])

When the specification mentions a pointer to member type, the traits used are like those above, except that each use of Pointer above is changed to PointerToMember, and each use of PointerToArray is changed to PointerToMemberArray.


Go to the first, previous, next, last section, table of contents.