两个数组相加校验超时

Question

我正在尝试验证两个二维数组的相加，但无论我使用何种解算器，我都会不断出现超时错误。

我要验证的代码如下：

typedef struct{
  float mem[3];
}BaseMatrix3x1;


/*@ requires \valid(b1) && \valid(b2);
  @ ensures A: \forall integer i; 0 <= i < 3 ==>
                b1->mem[i] == \old(b1)->mem[i] + b2->mem[i];
  @ assigns b1->mem[0..2];
@*/
void baseMatrixAssignAdd3x1(BaseMatrix3x1 *b1, BaseMatrix3x1 *b2){
    /*@ loop invariant 0 <= i <= 3;
      loop invariant \forall integer k; 
      0 <= k < i ==>
        \at(b1->mem[k], LoopCurrent) ==
            \at(b1->mem[k], LoopEntry) + \at(b2->mem[k], LoopEntry);
      loop assigns i, b1->mem[0..2];*/ 
    for(unsigned int i=0; i<3; i++){
        b1->mem[i] += b2->mem[i];
  }
}

第二个循环不变量是导致所有求解器超时的那个。

你有什么建议吗？

编辑：我修复了分配错误（虽然这不是问题）。

我还没有在某处调用这个函数，我只是想证明循环不变量。根据我的理解，为了验证一个函数，我们不关心这个函数被调用的方式。我们只关心我们拥有的 Pre 和 Post 条件。

Answer 1

首先，你的代码中incorrect/missing是什么：

你从来没有提到 b1 和 b2 是指向不同矩阵的指针。如果没有此信息，您的循环分配是不正确的，因为 b2->mem[0..2] 也会被分配。您需要添加一个 requires \separated(b1, b2); 假设
你的后置条件不正确，因为 \old 只适用于指针 b1 （无论如何在函数中保持不变），而它应该适用至 b1->mem。您应该改为 \old(b1->mem[i])。
你错过了一个重要的循环不变量，即 b1->mem[i..2] 还没有被修改（还）。由于您的循环分配提到所有 b1->mem 都可能在每次迭代时分配，因此您需要在未更改的部分上添加一个不变量。

接下来，WP 插件的一个明显限制阻止了完整证明：

对标签 LoopCurrent 的支持似乎不够。但是，在您的循环不变量中， LoopCurrent 是默认标签。所以你总是可以用 P.

\at(P, LoopCurrent)

这是 WP 插件能够证明的代码的完整注释版本，使用 Alt-Ergo 作为证明。

/*@
  requires \valid(b1) && \valid(b2);
  requires \separated(b1, b2);
  ensures A: \forall integer i; 0 <= i < 3 ==>
                b1->mem[i] == \old(b1->mem[i]) + b2->mem[i];
  assigns b1->mem[0..2];
@*/
void baseMatrixAssignAdd3x1(BaseMatrix3x1 *b1, BaseMatrix3x1 *b2){
  /*@ loop invariant 0 <= i <= 3;
      loop invariant \forall integer k; 
        k >= i ==> b1->mem[k] == \at(b1->mem[k], Pre);
      loop invariant \forall integer k; 
        0 <= k < i ==> b1->mem[k] == \at(b1->mem[k], LoopEntry) + b2->mem[k];
      loop assigns i, b1->mem[0..2];*/ 
  for(unsigned int i=0; i<3; i++){
    b1->mem[i] += b2->mem[i];
  }
}

两个数组相加校验超时

Timeout during the verification of two array addition

c

frama-c