2

当我尝试使用默认逻辑标签 LoopEntry 和 LoopCurrent 时，我遇到了一些麻烦。这是一个简单的示例，我使用的不同证明者（alt-ergo、coq、cvc3、z3）无法证明：

/*@ requires n > 0;*/
void f(int n){
    int i = 0;
    /*@ loop invariant \at(i,LoopEntry) == 0;
      @ loop invariant \at(i,LoopCurrent) >= \at(i,LoopEntry);
      @ loop invariant 0 <= i <= n;
      @ loop assigns i;
      @ loop variant n-i;
    */
    while(i < n){
        i++;
    }
}

特别是，第一和第二不变量没有被证明（其他没有问题）。现在，如果我通过在 i 的声明/定义之后添加标签“label”来修改这个简单的示例，并且如果我引用该标签，并通过 Here 更改 LoopCurrent （这给出了这个片段：

/*@ requires n > 0;*/
void f(int n){
    int i = 0;
    label : ;
    /*@ loop assigns i;
      @ loop invariant \at(i,label) == 0;
      @ loop invariant \at(i,Here) >= \at(i,label);
      @ loop invariant 0 <= i <= n;
      @ loop variant n-i;
    */
    while(i < n){
        i++;
    }
}

)

现在一切都被证明了。

我发现有关 Acsl 默认逻辑标签的文档很容易理解，并且我希望第一个示例被证明为第二个示例。你能解释一下问题出在哪里吗？

袋鼠

PS1：在循环子句中使用 Pre 时指的是什么？第一次循环迭代或上一次迭代之前的状态？？

PS2：我正在使用 Frama-C Fluorine，但也许我没有为每个小更新进行升级

4

1 回答 1

4

LoopCurrent并且LoopEntry确实不受 WP in Fluorine 的支持。这在开发版本中已修复（请参阅http://bts.frama-c.com/view.php?id=1353），并且应该会出现在下一个版本中。

关于其他预定义标签，

  • Pre总是指函数开始时的状态。
  • Old只能在合同中使用，指的是本合同的前置状态（即评估requiresandassumes条款的状态）。因此，它等同于Pre函数合约，但不等同于语句合约（除非您制作的合约包含函数的主块）。
  • Here表示评估相应注释的程序点。在合同中，其含义取决于其出现的条款。
  • Post只能用在ensures, assigns, allocatesorfrees子句中，指合同结束时的状态。
于 2013-09-04T15:04:46.717 回答