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.