验证两个阵列相加时超时

debugcn 发表于 Dev

埃尔德拉德

我正在尝试验证两个2d数组的相加，但是无论使用什么求解器，我都会不断遇到超时错误。

我要验证的代码如下：

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

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

你有什么建议吗？

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

我还没有在某处调用此函数，我只是在尝试证明循环不变式。据我了解，为了验证一个函数，我们并不关心该函数的调用方式。我们只关心我们拥有的前提条件。

其中

首先，代码中不正确/遗漏的是什么：

您永远不会提及它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。

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

/*@
  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];
  }
}

本文收集自互联网，转载请注明来源。

如有侵权，请联系[email protected] 删除。