Informally, an lcpp-primary of the form reach(x) denotes the
set of all objects reachable from x.
One way of thinking of this is that it is the set of objects
to which a pointer could be returned
by a C++ function that takes x as an argument.
This includes x itself.
For example, consider the following global variable declaration.
struct ratl { int num; int den; };
ratl r;
In the above example, reach(r) is a set containing
three type-tagged objects:
the object r itself,
and the num and den fields of r.
To formalize these intuitions, it is necessary for the Larch/C++ user
to explicitly say what objects are (directly) contained in each sort of
abstract value.
This is done by defining the trait function contained_objects.
For example, consider how this is done for a built-in C++ type.
The trait for struct ratl contains a definition of
a trait function contained_objects, which says that
in an abstract value r^, the directly contained objects
are r^.num and r^.den.
(To be technical, these are made into type-tagged objects,
see section 7.5 Contained Objects for details.
See section 11.10 Structure and Class Types for details of structs.)
The sort of the argument to reach
must be a sort of the form Obj[T] or ConstObj[T]
for some T.
The sort of the result is the sort Set[TypeTaggedObject].
(See section 6.2.3 The Modifies Clause for the trait TypeTaggedObject.)
Formally, the set of objects, reach(x),
is the smallest set such that the following holds.
asTypeTaggedObject(x) is in the set, and
asTypeTaggedObject(o),
is in the set, then
the set contained_objects(o^,pre) is a subset of the set.
(The type tag is needed here, because the exact version of
contained_objects depends on the sort of o,
which is recorded in a type-tagged object.)
See section 7.5 Contained Objects for the trait function
asTypeTaggedObject.
Go to the first, previous, next, last section, table of contents.