c - 验证两个数组相加时超时

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];
  }
}

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

你有什么建议吗？

编辑: 我修复了分配错误(但这不是问题)。

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

Answer 1

首先，您的代码中不正确/缺少什么:

• 您从未提到过 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 是默认标签。因此，您始终可以将 \at(P, LoopCurrent) 替换为 P。

这是 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];
  }
}