关于 ACSL 归纳谓词的 Coq 归纳推理？

Question

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

考虑以下来自 ACSL manual 的示例：

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))).

但是当我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 引理。

Answer 1

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

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

Answer 2

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

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

解决方法是提供一组适当的专用引理（无法通过 WP 证明）而不是归纳原理。参见例如binary_search_proved.c 在 this archive.

关于 ACSL 归纳谓词的 Coq 归纳推理？

Coq inductive reasoning about ACSL inductive predicates?

formal-verification

coq

frama-c

why3