The contained_objects trait function is generally useful in
a store-ref-list for extracting objects from abstract values
(as opposed to objects).
It is also the basis for a syntactic sugar in Larch/C++.
If the sort of a term listed in the store-ref-list
is not Set[TypeTaggedObject] or of the form Obj[T],
then the trait function contained_objects is applied,
to the value of the term and the pre-state
to obtain a set of type-tagged objects.
The set so obtained must be non-empty.
This is particularly helpful as a syntactic sugar
for C++ arrays and pointers,
and for structure and class types for which the default trait is used.
For global array variables (or fields of structures, etc. that are arrays),
the contained_objects trait function
returns a set of all the type-tagged objects that are the elements of
the array.
(See section 11.7 Array Types for details.)
The same functionality is provided by the trait function
contained_objects for pointers (and for arrays passed as parameters,
see section 11.8 Pointer Types).
Thus, in a store-ref-list Larch/C++ allows an array name
or pointer value as a store-ref.
When an array name or pointer value is mentioned in the modifies clause,
it is considered shorthand for all the elements of the array (pointed to).
For example, in the following, the modifies-clause is
shorthand for modifies contained_objects(ai, pre);.
// @(#)$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);
//@ }
Note that this shorthand names a wider range of objects than strictly necessary; it would be more accurate to write the following modifies-clause.
modifies objectsInRange(ai, 0, siz-1);
A similar shorthand applies to struct and class names
for which the default trait (see section 11.10 Structure and Class Types)
is used.
For example, by default
a struct global variable of type T is modeled in Larch/C++
as an object of sort ConstObj[T], and since the trait ConstObj
(see section 2.8.1 Formal Model of Objects) defines the contained_objects
trait function.
Thus if s is the name of a global variable that
is a struct of type T, then modifies s; is shorthand for
modifies contained_objects(s, pre);,
which says that all the fields of s can be modified,
as would be desired.
However, for structs within structs, one would have to
use reach, or some other term to state
that the subfields could also be modified.
This syntactic sugar applies to each sort with contained_objects
defined, which should be most sorts of values in Larch/C++.
An advantage of this approach is that it extends to user-defined types.
(Note that it is also consistent with the definition
of contained_objects for mutable objects.
See section 2.8.1 Formal Model of Objects for how contained_objects is defined for
mutable object sorts.)
A disadvantage is that few sort errors in the
modifies-clause will be caught,
because contained_objects should be defined for most sorts.
To have some error checking in the modifies-clause,
Larch/C++ considers it an error when the meaning of any store-ref
in a modifies-clause is the empty set of type-tagged objects.
Go to the first, previous, next, last section, table of contents.