If an object is assigned in a state (see section 6.2.2 Allocated and Assigned), then its abstract value can be obtained by using a state-function.
state-function ::=^|\pre|'|\post|\any|\obj
The value in the pre-state will be called the pre-value and the value in the post-state will be called the post-value.
For example, consider the following.
// @(#)$Id: add_one.lh,v 1.6 1997/06/03 20:29:55 leavens Exp $
extern void add_one(int& x) throw();
//@ behavior {
//@ requires assigned(x, pre) // x is allocated and has a value
//@ /\ x^ < INT_MAX; // x^ : pre-value of x
//@ modifies x; // x : an object
//@ ensures x' = x^ + 1; // x' : post-value of x
//@ }
Informally, add_one takes an integer object passed by reference,
and adds 1 to it.
More formally, assuming that x has a well-defined value,
and that the value of x in the pre-state
is not too large to be incremented, the post-value of x is
one greater than the original value of x.
The following table summarizes the sorts of terms using the different state functions.
term sort (assuming x declared as: int & x) ---- ------------------------------------- x Obj[int] x^ int x\pre int x' int x\post int x\any int x\obj Obj[int]
The state-functions ^ and \pre are synonymous,
and both are used to extract the pre-value of an object.
The state-functions ' and \post are synonymous,
and both are used to extract the post-value of an object.
For invariants (see section 7.3 Class Invariants)
and other situations where one wishes to extract
the value of an object,
but for which no particular visible state is appropriate,
the state-function \any can be used.
By a visible state we mean a state that a client can observe.
For a class with no public data members
(see section 2.3 Accessibility of Class Members in Specifications),
the visible states are the state just after an instance is created
and initialized by a creator,
and the states just before and just after the call
to any member function (or friend function),
in which the instance is passed.
For a class with public data members, every state is a visible state,
which is a good reason not to have public data members.
The state-function \obj can be used to explicitly refer to an
object itself, instead of its value.
It is essentially a no-op, and thus need only be used for emphasis.
Formally, the value of applying a state-function
to a value (which will usually be an object),
is given by passing the value and the appropriate
state to the trait function eval in the trait TypedObj
(see section 2.8.1 Formal Model of Objects for the trait TypedObj).
For example, i^ means eval(i,pre).
(See below for syntactic sugars that allow a state-function
to be applied to a value that is not an object.)
(One can also write eval(i,pre) in specifications.
However, i^ is shorter, and hence is the preferred form in Larch/C++.)
Except for syntactic sugars discussed below,
the state-functions can only be applied to terms that denote objects;
that is to terms whose sort has the form
Obj[T] or ConstObj[T] for some T.
The sort of a term with state-function \obj is unchanged,
but sorts ^, \pre, ', \post, and \any
take off the leading Obj or ConstObj sort generator.
You can only use a state-function on a formal parameter name
if that name parameter is passed by reference.
(More precisely, you can only use a state-function
on values for which the trait function eval is defined,
this is usually only object sorts.)
Value parameters are not considered objects in Larch/C++
(see section 6.1.8.1 Sorts for Formal Parameters)
and so the following is an error.
(See section 11.1 Integer Types for the trait function to_int.)
bool equal(int x, int y);
//@ behavior {
//@ ensures result = (x^ = y^); // error
//@ }
In the above example,
both x and y denote values not objects;
thus ^ cannot be used.
A legal ensures clause would be ensures result = (x = y);.
For C++ arrays,
one can apply a state-function to the elements of the array.
For example, the following specifies a function that
adds one to each element of an array.
Recall the sort of the formal parameter declared int ai[]
is Ptr[Obj[int]], because such C++ syntax means that a pointer
(into the array) is passed.
The term assignedUpTo(ai,siz) (see section 11.8 Pointer Types)
means that the pointer is not null, that the integers 0 to siz-1
(inclusive) are legal indexes for this pointer,
and that each element in that range is an allocated object
with a well-defined value.
Thus the pointer can be treated as an initialized array of size siz.
To avoid a syntax error,
a parenthesis is needed around ai[i] in terms like (ai[i])^.
This is because ai[i] is a secondary, and a state-function
can only be applied to a primary.
See section 6.1.7 Primaries for the syntax of primary.
See section 6.1.6 Brackets and Braces for the syntax of secondary.
// @(#)$Id: array_add_one.lh,v 1.12 1997/06/03 20:29:57 leavens Exp $
extern void array_add_one(int ai[], int siz) throw();
//@ behavior {
//@ requires 0 <= siz /\ assignedUpTo(ai, siz)
//@ /\ \A i:int ((0 <= i /\ i <= (siz-1))
//@ => (ai[i])^ + 1 <= INT_MAX);
//@ modifies ai;
//@ ensures \A i:int ((0 <= i /\ i <= (siz-1))
//@ => (ai[i])' = (ai[i])^ + 1);
//@ }
An array name (for global array variables), or a pointer formal,
such as ai in the above example,
is not an object.
However, as in LCL we extend the meaning of the state-functions to arrays
(and to pointers into arrays) element-wise.
In the context of array_add_one,
this extension makes ai' stand for
the abstract value of sort Arr[int]
that maps each legal index i of ai (if any) to (ai[i])'.
Note that the sort of ai' is not a pointer sort,
but an array sort.
In the above example, both (*ai)' and ai'[0]
would mean the same thing, and the syntax (ai[i])^
could be equivalently written as ai^[i] (or even (*(ai + i))^).
These syntactic sugars are defined because the trait function eval
is defined for pointers and arrays
in the traits Pointer (see section 11.8 Pointer Types)
and Array (see section 11.7 Array Types).
That is, ai'[i] is defined when the term (eval(ai,post))[i]
is defined,
because the latter is the desugared version of the former.
The sort Arr[int] is defined by the trait Array
(see section 11.7 Array Types),
which is included in the trait Pointer
(see section 11.8 Pointer Types).
The same sugar applies to multi-dimensional arrays.
For example, if aai is a two-dimensional array of ints
(declared as a global variable),
then aai' means eval(aai,post).
As defined in the trait MultiDimensionalArray
(see section 11.7 Array Types),
this is the abstract value of sort Arr[Arr[int]]
that assigns to each pair of legal indexs, i and j,
the abstract value ((aai[i])[j])'.
The same kind of sugar is defined for pointers to arrays.
See section 11.8 Pointer Types for details in the trait PointerToArray.
For C++ structures and classes that use the default (automatically-constructed) trait, one can apply a state-function to the fields of its abstract value. For example, consider the following global structure variable definition.
struct Ratl { int num, denom; };
Ratl my_ratl;
One can write my_ratl^.denom^, which has sort int,
because my_ratl^.denom is an object of sort Obj[int].
See section 11.10 Structure and Class Types for details on the
automatically constructed traits for structures and classes.
In the default traits for structures and classes,
Larch/C++ extends the meaning of the state-functions to
the tuples that are their abstract values element-wise.
Thus one can write my_ratl^^,
which means eval(eval(my_ratl,pre),pre);
because the trait function eval is defined on the sort
Ratl to return a value of sort Val[Ratl].
That is, my_ratl^^,
applies the state-function ^ to the tuple
that is the result of my_ratl^,
and is thus equal to the following.
[my_ratl^.num^, my_ratl^.denon^]
This last term denotes an abstract value of sort Val_Ratl,
containing the numerator and denominator values in the pre-state.
Hence my_ratl^^.num has sort int.
It follows that my_ratl^^.num and my_ratl^.num^
mean the same thing.
One way to see this is that my_ratl^.num has sort Obj[int],
because my_ratl^ is a tuple of objects.
See section 11.10 Structure and Class Types for more examples, and for details
of how the trait functions eval
and the sort Val[Ratl] are defined).
You may define a similar shorthand for the abstract values of a
type you specify the abstract values of explicitly
(see section 7 Class Specifications),
by specifying in LSL what the trait function eval means
for the abstract values.
Once this is done, the meaning of a state function gives the appropriate
shorthand.
Go to the first, previous, next, last section, table of contents.