Go to the first, previous, next, last section, table of contents. Reach

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.

See section 7.5 Contained Objects for the trait function asTypeTaggedObject.

Go to the first, previous, next, last section, table of contents.