Exercises

Minimizing replicated specifications Tutorial

Question 1

Consider the following class, which does not verify. Write one (or more) initially clauses so that it verifies. (Do not change any code or other specifications.)

// openjml --esc Inches.java
public class Inches {
    private /*@ spec_public @*/ double measure;
    
    //@ requires !Double.isNaN(inches);
    //@ requires 0.0 <= inches;
    public Inches(double inches) {
        measure = inches;
    }

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

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

** Answer these two questions about the above class.**

  • Why does it not verify?
  • Write an initially clause (or several initially clauses) for the class so that it verifies. Do not add any other specifications or change any code.

Question 2

Consider the following class, which does not verify. Write one (or more) constraint clauses so that it verifies. (Do not change any code or other specifications.)

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

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

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

}

Learning Objectives:

  • Gain more experience writing initially clauses.
  • Gain more experience writing constraint clauses.

Answer Key

Resources