10. Data Groups

A data group is a set of locations; data groups are used in JML's frame axioms (see section 9.9.9 Assignable Clauses) to name such sets of locations in a way that does not expose representation details [Leino98].

Each field in a program defines a data group, whose name is the same as that of the field.

The main purpose for putting locations into data groups is so that these locations may be assigned during the executions of methods that have permission to assign to the data group. For example, if locations x.f and x.y are in data group x.d, then an assignable clause of the form

assignable x.d;

allows x.d, x.f, x.y, and any other locations in the data group of x.d to be assigned during the execution of a method.

One should always put private or protected fields that are used to compute the value of a public model field (see section 8.4 Represents Clauses) into the data group of that model field. However, one can also put other fields into a model field's data group, just to allow them to be assigned when the model field is assignable.

It is sometimes convenient to declare a data group without any other information about the model of data. This can be done using the type org.jmlspecs.models.JMLDataGroup. This type has exactly one non-null object, named JMLDataGroup.IT. For example, the class java.lang.Object has the following data group declaration.

// public non_null model JMLDataGroup objectState;

The objectState data group provides a convenient way to talk about "the state" of an object without committing to any modeling or representation details.

[[[ needs discussion - default data groups ]]]

To place a field or array element in a data group, one uses the following syntax.

jml-data-group-clause ::= in-group-clause | maps-into-clause

The details of the two kinds of data group clauses are discussed below.

10.1 Static Data Group Inclusions
10.2 Dynamic Data Group Mappings

10.1 Static Data Group Inclusions

in-group-clause ::= in-keyword group-list ; in-keyword ::= in | in_redundantly group-list ::= group-name [ , group-name ] ... group-name ::= [ group-name-prefix ] ident group-name-prefix ::= super . | this .

The in-group-clause puts the field being declared in all the data groups named in the group-list.

[[[needs discussion]]]

10.2 Dynamic Data Group Mappings

See section 11.7 Store Refs, for the definition of spec-array-ref-expr.

maps-into-clause ::= maps-keyword member-field-ref \into group-list ; maps-keyword ::= maps | maps_redundantly member-field-ref ::= ident . maps-member-ref-expr | maps-array-ref-expr [ . maps-member-ref-expr ] maps-member-ref-expr ::= ident | * maps-array-ref-expr ::= ident maps-spec-array-dim [ maps-spec-array-dim ] ... maps-spec-array-dim ::= `[' spec-array-ref-expr `]'

The maps-into-clause describes elements of a data group that are determined dynamically, through a field reference or an array index, or a field of an array index. The pattern * may be used to specify all fields of an object or all elements of an array.

The fields of a model object do not denote locations because model objects are abstract and do not have concrete fields. Therefore, in JML, the maps clause is not allowed in the declaration of a model field because such maps clauses do not denote a specific set of locations to be added to a data group, and this is the primary purpose of the maps clause (see also the discussion of model fields in the assignable clause).

[[[ needs discussion ]]]