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 location (field or array element) in a program defines a data group, whose name is the same as that of the field or array element.

The main purpose for putting locations into data groups is so that these sets of locations may described succinctly in data groups by assignable clauses (see section 9.9.9 Assignable Clauses) 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.

JML requires users to put fields that are used to compute the value of a model field (see section 8.4 Represents Clauses) into the data group of that model field. This is especially useful for private and protected fields, since they would not be visible to clients who can see the public 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.lang.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. Fields are not automatically put into objectState by JML, (indeed, there is no default datagroup for a field), but it is often convenient to put fields into this datagroup.

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 12.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 meaning of a member-field-ref of the form E.* depends on the denotation of the ident or maps-array-ref-expr E. If E denotes a data group whose locations are objects, then E.* denotes the union of the data groups of all visible instance fields in E's (static) type. On the other hand, if E names a class or interface, then E.* denotes the union of the data groups of all visible static fields of the named class or interface.

Similarly, when E denotes a set of locations containing arrays, then E[*] denotes the union of all data groups of all elements in all the arrays denoted by E. Also, when E denotes a set of locations containing arrays, then E[L..H] denotes the union of all data groups of all elements in the arrays denoted by SR whose indexes are between L and H inclusive. In the case where E denotes a set of locations containing arrays, then E[J] denotes the union of all data groups of those arrays at the index denoted by the spec-expression J.

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 ]]]