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


6.2.3.2 Syntactic Sugars in the Modifies Clause

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.