Exercises:

Nullness Tutorial

Question 1

Consider the following code, which does not verify in JML.

// openjml --esc ObjPair.java
public class ObjPair {
    private Object fst, snd;

    public ObjPair(Object f, Object s) {
        //@ assume f != s;
        fst = f;
        snd = s;
        //@ assert fst == f && snd == s && fst != snd;
    }

    public static void test() {
        Integer five = Integer.valueOf(5);
        Integer seven = Integer.valueOf(7);
        ObjPair p = new ObjPair(five, seven);
        ObjPair oops = new ObjPair(null, seven); // <-- ERROR: this line wrong!
    }
}

(a) Why does the line marked as wrong in the method test() not verify?

(b) What could be done to the method test() to make the code verify?

(c) Aside from changing the method test(), what else could be done so that the program would verify?

Learning Objectives:

  • Understand JML’s defaults about non-null variables.
  • Understand how to fix code that has verification problems related to null.

Answer Key

Resources: