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.