Consider the following.
Declaration Name Its Sort (when used as a global variable) ------------- ---- ----------------------------------------- int ai[3]; ai Arr[Obj[int]]
The sort of ai, when used as a global variable,
is Arr[Obj[int]], which means that ai is an array
of integers.
In C++, an array variable can be thought of as the name of a sequence
of objects; however the array name is not itself an object.
Thus ai[0] is an object,
and so (ai[0])' is the value
of the zero-th element of the array in the state after the specified
function is called.
The sort of (ai[0])' is int,
while the sort of ai[0] is Obj[int],
which means that ai[0] is an integer object.
Since ai is not an object,
strictly speaking ai' should not have a meaning.
However, as in LCL (see Chapter 5 of [Guttag-Horning93]),
ai' stands for an abstract value
that maps each index i of ai to (ai[i])'.
See section 6.2.1 State Functions for details.
A declaration such as int ai[3] makes Larch/C++ implicitly include
the trait Array(Obj[int], int).
See section 11.7 Array Types for details of the traits
defining the abstract values of arrays,
and the instantiations used for various array types.
Go to the first, previous, next, last section, table of contents.