c - Frama-C 用 "/*@ ensures"证明 While 循环

Question

我是 Frama-C 的新手，我正在尝试验证 C 代码。代码非常基础，但不知何故我无法验证它。

总而言之，我试图证明该函数或循环是否曾经运行过。为此，我在开始时给一个变量一个值 (4)。在函数中，我将值更改为“5”，并尝试确保最后的变量为 5。

代码:

#include <stdio.h>
int x=4;
/*@
ensures x ==5;
*/
int abs(int val){

    int accept=0;
    int count=3;
    /*@
    loop invariant 0 <= count <= \at(count, Pre);
    loop assigns accept,x,count; 
    loop variant count;
    */
    while (count !=0){
        x=5;
        accept =1;
        count--;
    }
    return x;
 }

我将命令作为“frama-c-gui -wp -rte testp4.c”发送给 CLI 以启动 frama-c。

结果: Frama-1

但是“*@ ensures x ≡ 5; */”仍然未知。

有没有人可以帮我解决这个问题？如果我将 "x=5;" 带到 while 循环之外(在返回之前)，它会验证 /*@ 确保 x ==5; */

提前感谢所有做出贡献的人!

Answer 1

这里的大部分问题都与内置标签的使用有关。这里是我们需要的标签:

• Pre: 前提条件
• Post:后置条件中的状态
• LoopEntry:开始循环时的状态
• 此处:使用它的程序点的状态

要事第一。我不知道您使用的是哪个版本的 Frama-C，但我建议您更新 ;)。您将收到以下错误消息以防止出错:

[kernel:annot-error] file.c:11: Warning: 
  unbound logic variable count. Ignoring loop annotation

为什么？因为您在不存在的前提下谈论 count 。请注意，在旧版本的 Frama-C 中，WP 可能对此没有问题，因为在某些情况下合并了局部变量的预状态和初始化。

我们想要的可能是“count 的当前值介于 0 和我们开始循环时它的值之间的某处”，因此:

loop invariant 0 <= count <= \at(count, LoopEntry);
which is:
loop invariant 0 <= \at(count, Here) <= \at(count, LoopEntry);

现在我们有了这个(已证明的)不变量，我们想将循环的行为与后置条件联系起来(目前，我们的循环不变量没有说明任何关于 x 的信息，WP 不使用循环体。这意味着我们需要另一个不变量，即“当 count 不等于它在开始循环时的值时，x 是 5`” .

因此:

loop invariant count != \at(count, LoopEntry) ==> x == 5 ;

这允许完全证明程序 :) 。最终注释程序:

#include <stdio.h>
int x=4;
/*@
  ensures x ==5;
*/
int abs(int val){

  int accept=0;
  int count=3;
  /*@
    loop invariant 0 <= count <= \at(count, LoopEntry);
    loop invariant count != \at(count, LoopEntry) ==> x == 5 ;
    loop assigns accept,x,count; 
    loop variant count;
  */
  while (count !=0){
    x=5;
    accept =1;
    count--;
  }
  return x;
}

关于为什么 \at(count, Pre) != 0 ==>\at(x, Post) == 5 (在评论中)不起作用的一些说法:

• \at(count, Pre) 是 count 在 function 的前置条件中的值，\at(count, Post) 是函数的后置条件 中 count 的值。因此，这不是我们在这里需要的。