首页 文章

了解Frama-C逻辑标签

提问于
浏览 次
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，但也许我没有为每次小更新升级

frama-c

1 回答

  • 4

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

    关于其他预定义标签，

    • Pre 始终指的是函数开头的状态 .

    • Old 只能在 Contract 中使用，并且指的是本 Contract 的前置状态（即评估 requires 和 assumes 子句的状态） . 因此，对于函数 Contract ，它等效于 Pre ，但对于语句 Contract 则不等同（除非您签订了包含函数主块的合约） .

    • Here 表示评估相应注释的程序点 . 在 Contract 中，其含义取决于它出现的条款 .

    • Post 只能在 ensures ， assigns ， allocates 或 frees 子句中使用，并且可以参考 Contract 末尾的状态 .

    回复于

相关问题