javajmlopenjml

JML remove warning after calling a function

I'm given a task where I have to remove every warning produced by JML.
If I call a method inside the constructor my requires and ensures are not verified anymore, despite adding the same constraint for the called function.
I am asked to use only requires, ensures, invariant and loop_invariant.
Here is the code:

  /*@ non_null @*/ int[] elements;
  int n;
  //@ invariant n >= 0;
  
  //@ requires input != null;
  //@ requires input.length >= 0;
  //@ ensures elements != null;
  Class(int[] input) {
    n = input.length;
    elements = new int[n];
    arraycopy(input, 0, elements, 0, n);
    //@ assert n >= 0;
  }
  
  //@ requires srcOff >= 0;
  //@ requires destOff >= 0;
  //@ requires length >= 0;
  //@ requires dest.length >= destOff + length;
  //@ requires src.length >= srcOff + length;
  //@ ensures dest.length == \old(dest.length);
  //@ ensures length == \old(length) ==> length >= 0;
  //@ ensures dest != null;
  private static void arraycopy(/*@ non_null @*/ int[] src,
                                int   srcOff,
                                /*@ non_null @*/ int[] dest,
                                int   destOff,
                                int   length) {
     
     //@ loop_invariant destOff+i >= 0;
     //@ loop_invariant srcOff+i >= 0;
     //@ loop_invariant length >= 0;
     for(int i=0 ; i<length; i=i+1) {
        dest[destOff+i] = src[srcOff+i];
    }
  }

And the produced output:

Class.java:25: warning: The prover cannot establish an assertion (NullField) in method Class
  /*@ non_null @*/ int[] elements;
                         ^
Class.java:32: warning: The prover cannot establish an assertion (InvariantExit: MultiSet.java:27: ) in method Class
  Class(int[] input) {
  ^
Class.java:27: warning: Associated declaration: Class.java:32: 
  //@ invariant n >= 0;
      ^
3 warnings

One solution is to make the function arraycopy non-static but I can't understand why.

Solution

  • The prover cannot establish whether or not the class variables change as the function has visibility over n and elements. Thus it should need an annotation like

    //@ ensures n == \old(n)
//@ ensures elements == \old(elements)

    This is a problem for 2 different reasons:

    1. In Java a static method cannot access the value of a non-static variable, consequently the following specifications cannot be proven by JML (showing a tool limitation).
    // ...
//@ ensures n == \old(n)
//@ ensures elements == \old(elements)
private static void arraycopy( /* ... */ ) {
    1. The second ensures may cause some issues giving elements as src argoument for arraycopy.

    In order to avoid a modification of the function signature you'll need to add assume specification after every arraycopy function call.