为什么 OpenJML 不能在 for 循环中证明一个断言？答案

【问题标题】：Why OpenJML can not prove an assertion in for cycle?为什么 OpenJML 不能在 for 循环中证明一个断言？
【发布时间】：2020-12-14 15:13:11
【问题描述】：

我有以下代码：

//@ 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; 断言不起作用。它们在我看来还不错。

【问题讨论】：

标签： java jml openjml

【解决方案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];
    }
}

【讨论】：