4

例如，当使用带有选项 -wp-out 的 Frama-C WP 时（使用 swap.c 示例）：swap.c

// File swap.c:

/*@ requires \valid(a) && \valid(b);
  @ ensures A: *a == \old(*b) ;
  @ ensures B: *b == \old(*a) ;
  @ assigns *a,*b ;
  @*/

void swap(int *a,int *b)
{
  int tmp = *a ;
  *a = *b ;
  *b = tmp ;
  return ;
}

执行：

$frama-c -wp -wp-out po_out swap.c

并输出：

[jessie3] Loading Why3 configuration...
[jessie3] Why3 environment loaded.
[jessie3] Loading Why3 theories...
[jessie3] Loading Why3 modules...
[jessie3] Looking up module mach.int.Int32
[jessie3] Looking up module mach.int.Int64
[kernel] preprocessing with "clang -C -E -I.  swap.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 5 goals scheduled
[wp] [Qed] Goal typed_swap_post_B : Valid
[wp] [Qed] Goal typed_swap_assign_part1 : Valid
[wp] [Alt-Ergo] Goal typed_swap_assign_part2 : Valid (39ms) (21)
[wp] [Alt-Ergo] Goal typed_swap_post_A : Valid (Qed:1ms) (38ms) (13)
[wp] [Alt-Ergo] Goal typed_swap_assign_part3 : Valid (30ms) (21)
[wp] Proved goals:    5 / 5
     Qed:             2  (0ms-1ms)
     Alt-Ergo:        3  (30ms-39ms) (21)

它证明属性并生成一个文件夹，其中包含证明程序的属性所需的证明义务，但不是全部，只有那些发送给 Alt-ergo 的那些不会生成 Qed 证明的那些。

我了解 Qed 的目的是简化、证明琐碎的属性以节省证明者的时间和精力，但是是否可以让它生成所有的证明义务发送给证明者？也就是说，禁用 Qed 并让 Frama-C 生成对 alt-ergo 的所有证明义务？

4

1 回答 1

4

Qed有两个主要选项可以控制每个证明义务的工作量。的输出-wp-help给出了以下提示：

  • -wp-no-simpl防止简化常数项和谓词
  • -wp-no-let防止局部变量展开

如果您同时使用两者，您应该能够在您的po_out目录中获得大多数证明义务，或多或少是由 WP 计算出来的（请注意，某些 PO 可能仍会被解除Qed，例如，如果您有//@ assert \true;某个地方）。

于 2014-06-06T09:14:05.407 回答