#401 Non-Locally Bound Variables Cannot Be Used as Arguments

[jsinglet]

I ran into a very subtle bug:

Given the speced class:

public class ReadableInteger {


    protected /*@ spec_public non_null @*/ Integer value;

    //@ requires v != null;
    //@ ensures this.value !=null && this.value == v;
    public ReadableInteger(Integer v){
    this.value = v;
    }

    //@ ensures \result == this.value;
    public Integer getValue() {
    return this.value;
    }
}

If I try to write a class that uses like this:

public class GenericBug {

    public static void main(String args[]){

    ReadableInteger r = new ReadableInteger(new Integer(3));

    GenericBug b = new GenericBug();

    }

}

I get the error:

error: An error while executing a proof script for main: (error "Symbol _JML___NEWOBJECT_148_148 is already defined")
1 error

If I change the program to:

public class GenericBug {

    public static void main(String args[]){

    Integer a = new Integer(3);

    ReadableInteger r = new ReadableInteger(a);

    GenericBug b = new GenericBug();

    }

}

The program checks.

[Daniel M. Zimmerman]

As far as I can tell, your example works fine with the current released version of OpenJML. If it does not work for you with the current version, can you give some more details about your environment?

[Daniel M. Zimmerman]

Closing because this example worked for me 8 months ago, and still does.