1

是否可以对 ACSL 中定义的归纳谓词使用归纳？

考虑ACSL 手册中的以下示例：

struct List {
    int value;
    struct List* next;
};
/*@ inductive reachable{L}(struct List* root, struct List* to) {
  @   case empty{L}: \forall struct List* l; reachable(l, l);
  @   case non_empty{L}: \forall struct List *l1,*l2;
  @     \valid(l1) && reachable(l1->next, l2) ==> reachable(l1, l2);
  @ }
*/

我试图证明以下引理：

/*@ lemma next_null_reachable: \forall struct List* l;
  @   \valid(l) && reachable(l, \null) ==> reachable(l->next, \null);
*/

Alt-Ergo 在这里失败了，所以我求助于手动 Coq 推理：

Goal
  forall (t : array Z),
  forall (t_1 : farray addr addr),
  forall (a : addr),
  ((valid_rw t a 2%Z)) ->
  ((P_reachable t t_1 a (null))) ->
  ((P_reachable t t_1 (t_1.[ (shiftfield_F_List_next a) ]) (null))).

但是当 I 时Search P_reachable，我发现只生成了两个公理：

Q_non_empty:
  forall (t : array int) (t_1 : farray addr addr) (a_1 a : addr),
  valid_rw t a_1 2 ->
  P_reachable t t_1 (t_1 .[ shiftfield_F_List_next a_1]) a ->
  P_reachable t t_1 a_1 a
Q_empty:
  forall (t : array int) (t_1 : farray addr addr) (a : addr),
  P_reachable t t_1 a a

并且没有感应原理。所以我不能申请induction P_reachable或destruct P_reachable。

我使用frama-c版本 Sodium-20150201 的 WP 插件。

要重现，您可以运行frama-c -wp -wp-rte -wp-prover coqide file.c，其中file.c包含List和reachable定义和next_null_reachable引理。

4

2 回答 2

2

从您的目标形式来看，我假设您正在使用 WP 插件。实际上，它没有提供一个引理，表明 thatreachable是验证这两种情况的最小谓词empty和non_empty，这意味着您不能使用归纳法。

如果我没记错的话，添加这样一个公理会混淆一阶定理证明者（他们会反复构造reachablethrough的实例empty或non_empty用归纳原理破坏它们）。但是，WP 的 Coq 输出可以很好地提供完整的翻译。

一种解决方法是提供一组适当的专门引理（无法通过 WP 证明）而不是归纳原理。参见例如binary_search_proved.c在这个档案中。

于 2015-09-08T12:28:15.663 回答
0

我从未使用过 Alt-Ergo，但似乎它们并没有创建真正的归纳命题，而是将它们公理化。所以你不能这样做induction，但你可以使用它们提供的基本块（Q_empty是你的默认构造函数和Q_non_empty你的归纳构造函数）来执行证明。

我缺乏一些基本定义来重播你的问题，但我会申请Q_non_empty一次，这应该要求我证明一个valid_rw陈述和一个子P_reachable陈述。它们都应该可以使用您的上下文来证明。

于 2015-09-08T12:16:37.907 回答