The abstract value of a C++ array
is a mapping from indexes to objects.
As in C++, the index is 0-based.
For an array a, a[i] denotes the
i-th object of the array a, where
0 <= i <= maxIndex(a) and counting starts (as in C++) from zero (0).
The trait function maxIndex represents the upper bound of an array.
This basic idea is captured by the following trait.
% @(#) $Id: Val_Array.lsl,v 1.17 1995/08/11 21:38:30 leavens Exp $
% Mappings from integers to values (pre-arrays) with 0-based indexes
Val_Array(Elem): trait
includes int, % trait for C++ built-in type int.
Set(int, Set[int], int for Int)
introduces
create: int -> Arr[Elem]
allocated, allocatedUpTo: Arr[Elem], int -> Bool
allAllocated: Arr[Elem] -> Bool
allocatedInRange: Arr[Elem], int, int -> Bool
assign: Arr[Elem], int, Elem -> Arr[Elem]
__[__]: Arr[Elem], int -> Elem
maxIndex, minIndex: Arr[Elem] -> int
legalIndex: Arr[Elem], int -> Bool
size: Arr[Elem] -> int
slice: Arr[Elem], int, int -> Arr[Elem]
slice_helper: Arr[Elem], int, int, Arr[Elem], Set[int] -> Arr[Elem]
asserts
sort Arr[Elem] generated by create, assign
sort Arr[Elem] partitioned by size, allocated, __[__]
\forall a: Arr[Elem], i,j,n,siz: int, e: Elem
~allocated(create(n), j);
allocated(assign(a,i,e), j)
== legalIndex(a,j) /\ (i = j \/ allocated(a, j));
allAllocated(a) == allocatedInRange(a, 0, maxIndex(a));
allocatedInRange(a, i, j)
== i > j \/ (allocated(a, i) /\ allocatedInRange(a, i+1, j));
allocatedUpTo(a, siz) == allocatedInRange(a, 0, siz-1);
assign(a,i,e)[j] == (if i = j then e else a[j]);
maxIndex(assign(a,i,e)) == maxIndex(a);
maxIndex(create(n)) == n - 1;
minIndex(a) == 0;
legalIndex(a,i) == (0 <= i) /\ (i <= maxIndex(a));
size(create(n)) = n;
size(assign(a,i,e)) = size(a);
\forall a, a2: Arr[Elem], i, j, k: int, s: Set[int], e: Elem
slice(a,i,j)
== if i <= j then slice_helper(a, i, j, create(j-i), {})
else create(0);
slice_helper(create(k), i, j, a2, s) == a2;
slice_helper(assign(a,k,e), i, j, a2, s)
== if i <= k /\ k <= j /\ ~(k \in s)
then slice_helper(a, i, j, assign(a2,k,e), insert(k, s))
else slice_helper(a, i, j, a2, s);
implies
sort Arr[Elem] partitioned by maxIndex, allocated, __[__]
\forall a: Arr[Elem], i, j: int, e1, e2: Elem
assign(assign(a,i,e1),i,e2) == assign(a,i,e2);
i ~= j => assign(assign(a,i,e1),j,e2) = assign(assign(a,j,e2),i,e1);
allocated(a,i) => legalIndex(a,i);
size(a) == maxIndex(a) + 1;
j < 0 => (slice(a, i, j) = create(0));
converts allocated: Arr[Elem], int -> Bool,
allAllocated, allocatedInRange,
maxIndex, minIndex, legalIndex, size: Arr[Elem] -> int,
__[__]
exempting \forall n, i: int
create(n)[i]
The abstract values of arrays are defined using the trait Array
given below. It includes Val_Array twice.
The inclusion of Val_Array(Obj[Elem])
defines the sort Arr[Obj[Elem]] as a pre-array of objects;
this is the abstract value of a C++ array.
The inclusion of Val_Array(Elem)
defines the sort Arr[Elem] which is a pre-array of values;
this is used when a state function is applied to an array
(see section 6.2.1 State Functions).
% @(#) $Id: Array.lsl,v 1.38 1997/07/25 19:03:58 leavens Exp $
% Arrays as in C++, elements are some kind of object
Array(Loc, Elem): trait
includes Val_Array(Loc[Elem]), Val_Array(Elem),
ArrayAllocatedAuxFuns(Arr[Loc[Elem]]),
ArrayAssignedAuxFuns(Arr[Loc[Elem]]),
contained_objects(Arr[Loc[Elem]])
assumes TypedObj(Loc, Elem), contained_objects(Loc[Elem])
introduces
allocated, assigned: Arr[Loc[Elem]], int, State -> Bool
allocated, assigned: Arr[Loc[Elem]], State -> Bool
eval: Arr[Loc[Elem]], State -> Arr[Elem]
contained_without_indexes: Arr[Loc[Elem]], State, Set[int]
-> Set[TypeTaggedObject]
objectsInRange: Arr[Loc[Elem]], int, int -> Set[TypeTaggedObject]
objectsInRangeHelper: Arr[Loc[Elem]], Set[int] -> Set[TypeTaggedObject]
objectsUpTo: Arr[Loc[Elem]], int -> Set[TypeTaggedObject]
asserts
\forall a: Arr[Loc[Elem]], i,j,k,n,siz: int, e: Loc[Elem], st: State,
si: Set[int]
allocated(a, i, st) == allocated(a,i) /\ allocated(a[i], st);
assigned(a, i, st) == allocated(a,i) /\ assigned(a[i], st);
allocated(a, st) == allAllocated(a,st);
assigned(a, st) == allAssigned(a,st);
eval(create(i),st) == create(i);
eval(assign(a,i,e),st) == assign(eval(a,st), i, eval(e,st));
contained_objects(a, st)
== contained_without_indexes(a, st, {}:Set[int]);
contained_without_indexes(create(i), st, si) == {};
contained_without_indexes(assign(a,i,e), st, si)
== if i \in si then contained_without_indexes(a, st, si)
else {asTypeTaggedObject(e)}
\U contained_without_indexes(a, st, insert(i, si));
objectsInRange(a, i, j) == objectsInRangeHelper(slice(a,i,j), {});
objectsInRangeHelper(create(k), si) == {};
objectsInRangeHelper(assign(a,k,e), si)
== if k \in si then objectsInRangeHelper(a, si)
else {asTypeTaggedObject(e)}
\U objectsInRangeHelper(a, insert(k, si));
objectsUpTo(a, siz) == objectsInRange(a, 0, siz-1);
implies
\forall a: Arr[Loc[Elem]], i: int, e: Loc[Elem], st: State
size(contained_objects(a, st)) <= (maxIndex(a) + 1);
asTypeTaggedObject(e) \in contained_objects(assign(a,i,e), st);
converts
allocated: Arr[Loc[Elem]], int, State -> Bool,
assigned: Arr[Loc[Elem]], int, State -> Bool,
contained_objects: Arr[Loc[Elem]], State -> Set[TypeTaggedObject],
objectsInRange, objectsInRangeHelper, objectsUpTo
The trait Array also includes the trait ArrayAllocatedAuxFuns
to define various predicates to test whether objects are allocated.
% @(#)$Id: ArrayAllocatedAuxFuns.lsl,v 1.4 1995/08/24 21:30:19 leavens Exp $
ArrayAllocatedAuxFuns(T): trait
assumes int, State, ArrayAllocAuxSig(T)
introduces
allAllocated: T, State -> Bool
allocatedInRange: T, int, int, State -> Bool
allocatedUpTo: T, int, State -> Bool
asserts
\forall p: T, i,j,siz: int, st: State
allAllocated(p, st)
== allocatedInRange(p, minIndex(p), maxIndex(p), st);
allocatedInRange(p, i, j, st)
== i > j \/ (allocated(p, i, st) /\ allocatedInRange(p, i+1, j, st));
allocatedUpTo(p, siz, st) == allocatedInRange(p, 0, siz-1, st);
implies
converts
allAllocated: T, State -> Bool,
allocatedInRange: T, int, int, State -> Bool,
allocatedUpTo: T, int, State -> Bool
Some signature assumptions used by the trait ArrayAllocatedAuxFuns
are recorded in the trait ArrayAllocAuxSig.
% @(#)$Id: ArrayAllocAuxSig.lsl,v 1.1 1995/07/26 04:11:08 leavens Exp $
ArrayAllocAuxSig(T): trait
assumes int, State
introduces
allocated: T, int, State -> Bool
minIndex, maxIndex: T -> int
The trait Array also includes the trait ArrayAssignedAuxFuns
to define various predicates to test whether objects are assigned.
% @(#)$Id: ArrayAssignedAuxFuns.lsl,v 1.2 1995/11/13 22:35:34 leavens Exp $
ArrayAssignedAuxFuns(T): trait
includes
ArrayAllocatedAuxFuns(T,
assigned for allocated: T, int, State -> Bool,
allAssigned for allAllocated,
assignedInRange for allocatedInRange,
assignedUpTo for allocatedUpTo)
When an array type is used in a Larch/C++ specification,
an instantiation of the trait Array
is automatically used in the specification.
In this instantiation either Obj or ConstObj is substituted for
Loc, with the latter used if the elements are const,
and the value sort is substituted for Elem.
For example, an array declaration of the form
typedef Spigot Spigot_Vec[17];
makes the interface
specification use the trait
Array(Obj, Spigot).
The same holds true for an array variable declaration
(see section 5.4.3 Array Declarations).
For example, consider the following.
Declaration Trait used ----------------- -------------------------------------- int ai[3]; Array(Obj, int) const int cai[3]; Array(ConstObj, int) int *aip[3]; Array(Obj, Ptr[Obj[int]])
Recall that arrays used as formal parameters are equivalent to pointers; for such uses of array types, the equivalent pointer traits are used. (See section 11.8 Pointer Types for details on the abstract values of pointers.)
The objects directly contained in a one-dimensional array are the elements of the array.
A multi-dimensional array is modeled as an array of arrays.
More precisely, it is a mapping from integers to arrays.
For example, a two-dimensional array is a mapping from integers to arrays,
and a three-dimensional
array is treated as a mapping from integers to two-dimensional arrays
(hence it is like an array of arrays of arrays), and so on.
For example, int ai[3][4] declares an array of arrays of
integers, and ai[i] denotes i-th array and (ai[i])[j]
denotes j-th integer of the i-th array of ai;
maxIndex(ai) is 2 and for 0 <= i <= 2,
maxIndex(ai[i]) is 3.
Note that ai is of sort Arr[Arr[Obj[int]]], ai[i]
is of sort Arr[Obj[int]], and (ai[i])[j] is of sort
Obj[int] (see section 5.4.8 Summary of Declarations).
The trait used in defining multi-dimensional arrays is
the trait MultiDimensionalArray that follows.
% @(#) $Id: MultiDimensionalArray.lsl,v 1.27 1999/01/12 22:40:17 leavens Exp $
% Supplement for higher dimensions of an array in C++
MultiDimensionalArray(SubObjArr, SubValArr): trait
assumes State, SubArray(SubObjArr, SubValArr)
includes Val_Array(SubObjArr), Val_Array(SubValArr),
NoContainedObjects(Arr[SubValArr]),
ArrayAllocatedAuxFuns(Arr[SubObjArr]),
ArrayAssignedAuxFuns(Arr[SubObjArr]),
contained_objects(Arr[SubObjArr])
introduces
allocated, assigned: Arr[SubObjArr], int, State -> Bool
eval: Arr[SubObjArr], State -> Arr[SubValArr]
contained_without_indexes: Arr[SubObjArr], State, Set[int]
-> Set[TypeTaggedObject]
objectsInRange: Arr[SubObjArr], int, int -> Set[TypeTaggedObject]
objectsInRangeHelper: Arr[SubObjArr], Set[int] -> Set[TypeTaggedObject]
objectsUpTo: Arr[SubObjArr], int -> Set[TypeTaggedObject]
asserts
\forall a: Arr[SubObjArr], i,j,k,n,siz: int, e: SubObjArr, st: State,
si: Set[int]
allocated(a, i, st) == allocated(a,i) /\ allAllocated(a[i], st);
assigned(a, i, st) == allocated(a,i) /\ allAssigned(a[i], st);
eval(create(n): Arr[SubValArr], st) == create(n);
eval(assign(a,i,e),st) == assign(eval(a,st), i, eval(e,st));
contained_objects(a, st)
== contained_without_indexes(a, st, {}:Set[int]);
contained_without_indexes(create(i) : Arr[SubObjArr], st, si) == {};
contained_without_indexes(assign(a,i,e), st, si)
== if i \in si then contained_without_indexes(a, st, si)
else contained_objects(e, st)
\U contained_without_indexes(a, st, insert(i, si));
objectsInRange(a, i, j) == objectsInRangeHelper(slice(a,i,j), {});
objectsInRangeHelper(create(k), si) == {};
objectsInRangeHelper(assign(a,k,e), si)
== if k \in si then objectsInRangeHelper(a, si)
else objectsInRange(a[k], 0, maxIndex(a[k]))
\U objectsInRangeHelper(a, insert(k, si));
objectsUpTo(a, siz) == objectsInRange(a, 0, siz-1);
implies
\forall a: Arr[SubObjArr], st: State
size(contained_objects(a, st)) <= (maxIndex(a) + 1);
converts
allocated: Arr[SubObjArr], int, State -> Bool,
assigned: Arr[SubObjArr], int, State -> Bool,
contained_objects: Arr[SubObjArr], State -> Set[TypeTaggedObject],
objectsInRange: Arr[SubObjArr], int, int -> Set[TypeTaggedObject],
objectsUpTo: Arr[SubObjArr], int -> Set[TypeTaggedObject]
The trait SubArray is included by MultiDimensionalArray
as a shorthand for some signature assumptions.
% @(#) $Id: SubArray.lsl,v 1.14 1995/11/06 07:19:07 leavens Exp $
SubArray(SubObjArr, SubValArr): trait
assumes State
includes contained_objects(SubObjArr)
introduces
allAllocated, allAssigned: SubObjArr, State -> Bool
eval: SubObjArr, State -> SubValArr
objectsInRange: SubObjArr, int, int -> Set[TypeTaggedObject]
maxIndex: SubObjArr -> int
Instantiations of the trait MultiDimensionalArray are implicitly
used in the interface specification module in which the declaration appears.
For example, consider the following.
Declarations Traits to be used
------------- ----------------------------------------------------
int x[3][4]; Array(Obj, int),
MultiDimensionalArray(Arr[Obj[int]], Arr[int])
const int cx[3][4]; Array(ConstObj, int),
MultiDimensionalArray(Arr[ConstObj[int]], Arr[int])
int x[5][3][4]; Array(Obj[int], int),
MultiDimensionalArray(Arr[Obj[int]], Arr[int]),
MultiDimensionalArray(Arr[Arr[Obj[int]]], Arr[Arr[int]])
A one-dimensional array is a collection of objects (not values),
so to describe the abstract value of an element one has to apply
a state-fcn to that element.
For example, (a[i])^ denotes the pre-state value of a[i].
See section 5.4.3 Array Declarations for an overview.
See section 6.2.1 State Functions for the details.
There is a shorthand notation for applying a state function element-wise to an array, See section 6.2.1 State Functions.
See section 6.2.3 The Modifies Clause for a shorthand that allows one to assert that one can mutate any element object of an array, not just a particular element object.
Go to the first, previous, next, last section, table of contents.