VisibilityAndStoreRefs

Visibility and Store-Refs

There was an email discussion following the Shonan meeting in May 2013 about the meaning of .* in a store-ref, in particular with respect to the visibility rules. In essence we decided that .* refers to the visible fields and hence their datagroups. However, we also decided that the default assignable clause for a constructor, namely this.* should not refer to static fields of the class of this. Thus, if a specifier wants to allow static fields to be assigned in a constructor, they must write an explicit assignable clause.

[The results of this discussion are recorded in the JML Reference Manual]

There is a continuing question about the interaction of .* and inheritance of fields in Java. Gary's position on that is that "visible fields" includes inherited fields, certainly for objects/instances. However, this is not so clear for static fields, since some might say that in T.*, where T names a type, then the static fields should also include static fields in all supertypes of D, as static fields are "inherited" in some sense from interfaces and superclasses in Java.