使用Jessie插件和Frama-C的验证问题

Question

我是 Frama-C 的新手，我想正确学习 ACSL 语法。我有这个虚拟示例，Jessie 插件无法验证第 9 行和第 12 行。我是否遗漏了什么？要验证的函数(等于)将检查两个数组(a 和 b)在每个索引处是否具有相同的值:

/*@
     requires \valid_range(a,0,n-1);
     requires \valid_range(b,0,n-1);
     requires n >= 0;
     requires i >= 0 && i <= n;
     assigns i;
     behavior all_equal:
         assumes i == n;
         ensures \result == 1;
     behavior some_not_equal:
        assumes i != n;
        ensures \result == 0;
*/
int equal(int a[], int n, int b[], int i) {
  /*@ 
    loop invariant 0 <= i <= n;
    loop assigns i;
    loop variant n-i;
  */  
  for (i = 0; i < n; i++) {
    if (a[i] != b[i])
      return 0;
  }
  return 1;
}

Answer 1

这里有一些不正确的地方:

behavior all_equal:
     assumes i == n;
     ensures \result == 1;
 behavior some_not_equal:
    assumes i != n;
    ensures \result == 0;

在assumes 子句中，所有变量都在函数的预状态中求值。这意味着如果您有两个大小相同的数组 n，并且假设 i 是 0(这不可能，请参阅下一个解释)，i == n 将始终失败，除非数组的大小为 0

另一件事:您似乎正在使用 i 作为循环控制的变量，在循环开始时将其设置为 0，但是在您的注释中您说 i，在程序的预状态中，介于0和n之间。这与我之前所说的相结合是杰西无法证明这一点的原因之一。

最后，您无法证明这一点的主要原因是因为您缺少一个基本的循环不变量，它保证两个数组对于当前迭代之前的所有数组索引都是相等的:

loop invariant loop invariant \forall integer k; 0 <= k < i ==> a[k] == b[k];

有了这个不变量，您现在可以更好地指定您的行为。针对您的问题的正确解决方案是:

/*@
     requires \valid_range(a,0,n-1);
     requires \valid_range(b,0,n-1);
     requires n >= 0;
     behavior all_equal:
         assumes \forall integer k; 0 <= k < n ==> a[k] == b[k];
         ensures \result == 1;
     behavior some_not_equal:
        assumes \exists integer k; 0 <= k < n  && a[k] != b[k];
        ensures \result == 0;
*/
int equal(int a[], int n, int b[]) {
  int i = 0;
  /*@ 
    loop invariant 0 <= i <= n;
    loop invariant \forall integer k; 0 <= k < i ==> a[k] == b[k];
    loop assigns i;
    loop variant n-i;
  */  
  for (i = 0; i < n; i++) {
    if (a[i] != b[i])
      return 0;
  }
  return 1;
}