Why OpenJML can not prove an assertion in for cycle?

Question

I have the following piece of code:

//@ requires dest != null;
//@ requires srcOff >= 0;
//@ requires destOff >= 0;
//@ requires length >= 0;
//@ requires srcOff < src.length;
//@ requires destOff < dest.length;
//@ requires srcOff + length <= src.length;
//@ requires destOff + length <= dest.length;
//@ ensures dest != null;
//@ ensures src != null;
//@ ensures \old(length) == length;
//@ ensures \old(dest.length) == dest.length;
//@ ensures (\forall int j; 0 <= j && j < length; dest[destOff+j] == src[srcOff+j]);
private static void arraycopy(int[] src,
                              int   srcOff,
                              int[] dest,
                              int   destOff,
                              int   length) {
  int i = 0;                              
  for(i=0 ; i<length; i=i+1) {
    //@ assert length >= 0;
    //@ assert i < length;
    //@ assert i >= 0;
    //@ assert destOff + i >= 0;
    //@ assert srcOff + i >= 0;
    //@ assert destOff + i < dest.length;
    //@ assert srcOff + i < src.length;
    dest[destOff+i] = src[srcOff+i];
  }
}

in which I have inserted some OpenJML annotations. When i run OpenJML on therminal, I obtain the following errors:

$ jml -esc MultiSet.java 
MultiSet.java:120: warning: The prover cannot establish an assertion (Postcondition: MultiSet.java:119: ) in method arraycopy
  private static void arraycopy(int[] src,
                      ^
MultiSet.java:119: warning: Associated declaration: MultiSet.java:120: 
  //@ ensures (\forall int j; 0 <= j && j < length; dest[destOff+j] == src[srcOff+j]);
      ^
MultiSet.java:129: warning: The prover cannot establish an assertion (Assert) in method arraycopy
      //@ assert i >= 0;
          ^
3 warnings

I really can't understand why the \forall cycle and the //@ assert i >= 0; assertion are not working. They look okay to me.

score 2 · Accepted Answer · answered Dec 21 '20 at 00:34

Use loop invariants, since they provide loop preconditions (assumptions) that are used to establish assertions. You need to specify all of the invariants related to every variable that is being modified. Also, you need an extra condition requires src != dest, because the prover can run into an aliasing problem, and avoid using a lot of index arithmetic in the assertions, see https://github.com/OpenJML/OpenJML/issues/716 (special thanks to David Cok for this clarification, one of the maintainers of OpenJML).

Here is a version of your method with proper contract and loop invariants that is verifiable:

/*@
 requires src != dst;
 requires 0 <= len && len <= src.length-srcOfs && len <= dst.length-dstOfs;
 requires 0 <= srcOfs && srcOfs < src.length;
 requires 0 <= dstOfs && dstOfs < dst.length;
 ensures \forall int k;0 <= k && k < len;dst[dstOfs + k] == src[srcOfs + k];
 @*/
public static void CopyArray(final /*@non_null \readonly @*/ int [] src, final int srcOfs, 
                /*@ non_null @*/int [] dst, final int dstOfs,
                final int len) {
    //@ loop_invariant 0 <= i && i <= len;
    //@ loop_invariant \forall int k;0 <= k && k < dstOfs; dst[k]==\old(dst[k]);
    //@ loop_invariant \forall int k; dstOfs+i <= k && k < dst.length; dst[k]==\old(dst[k]);
    //@ loop_invariant \forall int k;dstOfs <= k && k < dstOfs+i;dst[k] == src[srcOfs-dstOfs+k];
    //@ decreasing len-i;
    for(int i = 0;i < len;i++) {
        dst[dstOfs+i] = src[srcOfs+i];
        //@ assert dst[dstOfs+i]==src[srcOfs+i];
    }
}

Why OpenJML can not prove an assertion in for cycle?

1 Answers1