Exercises

Minimizing replicated specifications Tutorial

Question 1

The following is one way to answer this question.

// openjml --esc InchesAns.java
public class InchesAns {
    private /*@ spec_public @*/ double measure;

    //@ public initially !Double.isNaN(measure);
    //@ public initially 0.0 <= measure;
    
    //@ requires !Double.isNaN(inches);
    //@ requires 0.0 <= inches;
    public InchesAns(double inches) {
        measure = inches;
    }

    //@ old double epsilon = 0.1e-9;
    //@ requires !Double.isNaN(oth);
    //@ requires 0.0 <= oth;
    //@ requires 0 < multiple;
    //@ ensures Math.abs(measure - multiple*oth) < epsilon;
    public InchesAns(double oth, int multiple) {
        measure = multiple * oth;
        //@ assume !Double.isNaN(measure); // only needed temporarily.
    }

    public void test() {
        InchesAns i = new InchesAns(3.0);
        //@ assert 0.0 <= i.measure;
        InchesAns f = new InchesAns(5.0, 12);
        //@ assert 0.0 <= f.measure;
    }
}

Note that the above uses two initially clauses, this is equivalent to conjoining the first to the second using &&.

Question 2

The following is one way to answer this question.

// openjml --esc LogAns.java
public class LogAns {
    private /*@ spec_public @*/ String text = "";

    //@ public constraint \old(text.length()) <= text.length();

    //@ assignable text;
    //@ ensures text == \old(text + s);
    public void add(String s) {
        text += s;
    }

    public void test() {
        LogAns l = new LogAns();
        l.add("something");        
        int oldlen = text.length();
        l.add("something else");
        //@ assert oldlen <= text.length();
    }

}

Depending on the version of OpenJML used, this may still not verify, because some of the operations on the built-in type String may not have been implemented yet in the tool.

Resources