为什么 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 注释。当我在 therminal 上运行 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（特别感谢 David Cok 对此进行了澄清，OpenJML 的维护者之一）。

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

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

为什么 OpenJML 无法证明 for 循环中的断言？

Why OpenJML can not prove an assertion in for cycle?

java

jml

openjml