VisibilityAndImmutability

David Cok (in a post to jmlspecs-interest on May 18, 2013) raised the following issues with respect to the privacy rules and immutable data:

The privacy rules (see the ICSE 2007 paper by Leavens and Mueller http://dx.doi.org/10.1109/ICSE.2007.44) say that class members mentioned in an invariant (for example) must have the same visibility as the invariant -- no more and no less.
But the situation arises where invariants refer to constant, immutable data, which may well be public. Suppose that the immutable data (e.g., a final field) is public, but the invariant has less visibility.
This doesn't seem to cause a problem, but the paper referred to above doesn't consider it.

In implementing these privacy rules I also had to handle other special cases - such as top-level type and package names, this, super, the 'length' field of an array.

Gary Leavens wrote in response:

I believe you are right that we did not consider constant immutable data in our paper on visibility in specifications. I agree that as long as the field itself is final and the data in the field is immutable, then it is okay for an invariant to refer to it if the field is at least as visible as the data and is final, and the data is immutable.

David's response to this was:

If we allow immutable stuff of any visibility, then that covers:

• lengths of arrays
• package and class names (but not their fields).

The names this and super seem to be unusual cases and deserve some careful thinking, but it seems they have to be visible everywhere.

At Shonan, Dan was complaining about this rule as it would apply to pure methods, also not considered in the privacy paper. After writing some specs using OpenJML (which has these visibility rules in it), he thought the restrictions on the use of pure methods to be unworkable.