在 Java 中使用 'KeY' 进行形式验证无法证明数组重置循环

Question

当前我正在尝试使用Java程序的键工具来掌握一些正式验证。

这是我的密钥注释的Java代码：

public class Test {
    public int[] a;
    /*@ public normal_behavior
    @ ensures (forall int x; 0<=x && x<a.length; a[x]==1);
    @*/
    public void fillArray() {
        int i = 0;
        while(i < a.length) {
            a[i] = 1;
            i++;
        }
    }
}

令我惊讶的是键，它无法证明当前程序根据其规范有效。键在目标上失败54.当前目标窗口显示：

 self.a.<created> = TRUE,
 wellFormed(heap),
 self.<created> = TRUE,
 Test::exactInstance(self) = TRUE,
 measuredByEmpty
==>
 self.a = null,
 self = null,
 {exc:=null || i:=0}
   <{
         try {
             method-frame(source=fillArray()@Test, this=self)
             : {
                 while (i<this.a.length) {
                   this.a[i] = 1;
                   i++;
                 }
               }
         }
         catch (java.lang.Throwable e) {
             exc = e;
         }
     }> (forall int x; (x <= -1 | x >= self.a.length | self.a[x] = 1) & self.<inv> & exc = null)

我没有真正理解：无法证明规范的主要原因是什么？

Answer 1

失败的最基本原因是，如果供者在方法中找到了一个无限的循环 - 那么如果没有循环不变规范，它就无法遵循方法规范。

因此，对于每个无界环，我们必须指定一个循环不变。循环不变是某种规则，每个规则都为每个循环迭代保存true 。每个循环都可以具有自己的特定不变规则。因此，必须将带规范的Java代码固定为：

public class Test{
  public int[] a;
  /*@ public normal_behavior
  @ ensures (forall int x; 0<=x && x<a.length; a[x]==1); // method post-condition
  @ diverges true; // not necessary terminates
  @*/
  public void fillArray() {
    int i = 0;
    /*@ loop_invariant
    @ 0 <= i && i <= a.length &&  // i ∈ [0, a.length]
    @ (forall int x; 0<=x && x<i; a[x]==1); // x ∈ [0, i) | a[x] = 1
    @ assignable a[*]; // Valid array location
    @*/
    while(i < a.length) {
      a[i] = 1;
      i++;
    }
  }
}

思考如何指定方法的最难部分是发现循环不变。但与此同时 - 这是最有趣的。出于原因，我将重复此循环的不变式：

i＆nbsp;∈[0，a.length]
x∈[0，i）|a [x] = 1

这种情况永远不会在>>>迭代中的循环中变化。这就是为什么它是不变。

btw，如果正式规范是正确 - 我们可以丢弃TDD，并将单位测试掉出窗口。谁在关心运行时结果，如果程序可以根据其规范被数学证明是正确的？

如果规范很好，并且代码语义是 precen - 然后在程序执行中可能会出错 - 这是可以肯定的。因此 - 正式验证是一个非常有前途的领域。