JML Tutorial - Visibility modifiers and specifications

Java distinguishes four categories of visibility of declarations: public, protected, package, and private. For example, within a class, all names, even private ones, declared in that class are visible. But names private to one class are not visible outside that class.

Specifications have a visibility also. By default a method specification has the same visibility as the method declaration. That way a client seeing the method declaration can see its specification also. But if that client is not permitted to see names with more restricted visibility, then those names should not appear in the specifications either.

For example, this code

// openjml --esc T_Visibility1.java
public class T_Visibility1 {
    private int _value;

    //@ ensures \result == _value;
    public int value() {
        return _value;
    }
}

violates JML’s visibility rules because a client that can see the public declaration of the method value() does not necessarily have visibility to the private declaration of _value. This error results:

T_Visibility1.java:5: error: An identifier with private visibility may not be used in a ensures clause with public visibility
    //@ ensures \result == _value;
                           ^
1 error

So how is one to specify this simple getter method? The simple solution is simply to declare that the private field is public for specification purposes. The spec_public declaration does this:

// openjml --esc T_Visibility2.java
public class T_Visibility2 {
    //@ spec_public
    private int _value;

    //@ ensures \result == _value;
    public int value() {
        return _value;
    }
}

which now verifies without error.

There is a similar modifier, spec_protected, that declares that a declared name has protected visibility for specification purposes.

But this solution leads easily to simply declaring all names as spec_public; however, that may not make the specification easy to understand for the reader (especially if the private fields have been optimized for algorithmic reasons). In cases where the data structure is complex or not easily understood by a client, then it may be best to only allows clients access to the data through public methods. So, we need a specification idiom that respects that, which is one purpose of model fields, which are presented in a subsequent lesson¹. But here we’ll repeat our example using a model field.

// openjml --esc T_Visibility3.java
public class T_Visibility3 {
    private int _value; //@ in value;

    //@ public model int value;
    //@ private represents value = _value;

    //@ ensures \result == value;
    public int value() {
        return _value;
    }
}

The general point is this. The model field value models the state of the class object, as a public abstraction. The represents clause, which is private, tells how the abstraction relates to concrete (private) fields. The specification of value() only uses the public abstraction value. Of course, in this case, the abstraction is quite trivial. In fact, the goal of the private _value field is not so much implementation hiding but preventing access to the data field, that is, not allowing clients to modify _value directly. So for simple cases like this the spec_public modifier is perfectly fine; in fact, it is syntactic sugar for the solution in terms of a model field.

Exercises

Follow the link in the above heading to work on the exercises on this topic.

Resources

• T_Visibility1 file
• T_Visibility2 file
• T_Visibility3 file

Footnotes