为什么OpenJML不能证明for循环中的断言？

Question

我有下面这段代码：

//@ 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];
  }
}

我在其中插入了一些OpenJML注释。当我在终端上运行OpenJML时，我得到了以下错误：

$ 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

我真的不明白为什么\forall循环和//@ assert i >= 0;断言不起作用。在我看来还可以。

Answer 1

使用循环不变量，因为它们提供了用于建立断言的循环前提条件(假设)。您需要指定与正在修改的每个变量相关的所有不变量。此外，您还需要一个额外的条件requires src != dest，因为证明者可能会遇到别名问题，并避免在断言中使用大量的索引算法，请参阅https://github.com/OpenJML/OpenJML/issues/716 (特别感谢OpenJML的维护者之一David Cok对此进行了澄清)。

以下是您的方法的一个版本，它具有适当的约定和循环不变量，是可验证的：

/*@
 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];
    }
}