调用函数后 JML 删除警告答案

【问题标题】：JML remove warning after calling a function调用函数后 JML 删除警告
【发布时间】：2021-03-24 05:20:21
【问题描述】：

我接到了一项任务，我必须删除 JML 产生的所有警告。
如果我在构造函数中调用一个方法，我的requires 和ensures 将不再被验证，尽管为被调用函数添加了相同的约束。
我被要求仅使用 requires、ensures、invariant 和 loop_invariant。
代码如下：

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

以及产生的输出：

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

一种解决方案是使函数arraycopy 非静态，但我不明白为什么。

【问题讨论】：

标签： java jml openjml

【解决方案1】：

证明者无法确定类变量是否随着函数对n 和elements 的可见性而改变。因此它应该需要像

这样的注释

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

这个问题有两个不同的原因：

在 Java 中，静态方法无法访问非静态变量的值，因此 JML 无法证明以下规范（显示工具限制）。

// ...
//@ ensures n == \old(n)
//@ ensures elements == \old(elements)
private static void arraycopy( /* ... */ ) {

第二个ensures 可能会导致一些问题，将elements 作为src 参数为arraycopy。

为了避免修改函数签名，您需要在每个 arraycopy 函数调用之后添加 assume 规范。

【讨论】：