Почему 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

Используйте инварианты цикла, так как они обеспечивают предварительные условия цикла (допущения), которые используются для установления утверждений. Вам необходимо указать все инварианты, относящиеся к каждой изменяемой переменной. Кроме того, вам нужно дополнительное условие , потому что доказывающий может столкнуться с проблемой алиасинга и избежать большого количества индексных арифметических операций в утверждениях, см. https://github.com/OpenJML/OpenJML/issues/716 (особая благодарность Дэвиду Коку за это разъяснение, один сопровождающих 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];
    }
}