如何在Isabelle/HOL中证明while/for

Question

我有这段C代码：

while(p->next)   p = p->next;

我想证明无论列表有多长，在此循环结束时，p->next 等于 NULL，且 EIP 指向此循环后的下一条指令。

但是我不知道怎样证明在 Isabelle/HOL 中的循环。

- njuguoyi

---

我不知道在Isabelle/HOL中有任何直接证明C代码属性的方法。您能否提供更多关于您试图实现什么以及您使用了什么（或期望使用什么）来实现此目的的详细信息？也许http://afp.sourceforge.net/entries/Simpl.shtml会对您有所帮助。顺便问一下：“EIP”是什么？ - chris

无论您想使用哪种证明工具，您打算如何处理列表是循环的情况（即，循环不会终止）？ - chris

你好 @chris。很抱歉我不能告诉你太多细节，因为这是一个团队合作项目，也还未发布。但我可以告诉你的是，我们正在用 Isabelle 模拟 X86 ISA 指令，如 mov、jmp 等。由 gcc 生成的汇编代码会被转译成 Isabelle，并在其中运行。如果没有循环，结果非常好。但我们无法处理循环，因为它更为困难。我们希望证明对于所有的 n，这个 while 循环最终将导致 p->next 等于 NULL，而 eip（pc）将指向循环下面的下一条指令。 - njuguoyi

我不是在询问您项目的细节，只需要更多上下文信息，例如您正在使用 Isabelle 的哪个逻辑，如何将 C 代码导入 Isabelle 等等。如果没有这些信息，您的问题将不能容易地得到答复。 - chris

Answer 1

一组工具（免责声明：我是后者的作者），可以将C代码导入Isabelle/HOL中以进行进一步的推理，这些工具包括Michael Norrish的C Parser和AutoCorres。

使用AutoCorres，我可以解析以下C文件：

struct node {
    struct node *next;
    int data;
};

struct node * traverse_list(struct node *list)
{
    while (list)
        list = list->next;
    return list;
}

使用以下指令将其转换为 Isabelle：

theory List
imports AutoCorres
begin

install_C_file "list.c"
autocorres [ts_rules = nondet] "list.c"

接下来，我们可以证明一个 Hoare 三元组，它声明对于任何输入状态，函数的返回值将为 NULL：

lemma "⦃ λs. True ⦄ traverse_list' l ⦃ λrv s. rv = NULL ⦄"
  (* Unfold the function definition. *)
  apply (unfold traverse_list'_def)

  (* Add an invariant to the while loop. *)
  apply (subst whileLoop_add_inv [where I="λnext s. True"])

  (* Run a VCG, and solve the conditions using the simplified. *)
  apply wp
  apply simp
  done

这是一个部分正确性定理，有点陈述了您所要求的内容。(特别地，它表明如果函数终止，且如果它不出错，那么后置条件是真实的)。

要进行更完整的证明，您需要在上述内容中增加一些内容:

1. 您需要知道列表是有效的；例如，中间节点不指向无效地址（例如，未对准的地址），并且列表不形成循环（意味着while循环永远不会终止）。

2. 您还需要证明终止性。这与上面的第二个条件有关，但您可能仍然需要证明它为什么是正确的。（一种典型的方法是说列表的长度总是减少，因此循环最终将终止）。

AutoCorres没有指令指针的直接概念（通常这些概念只存在于汇编级别），但是终止证明类似。

AutoCorres提供了一些关于链表推理的基本库，在中，这将是一个很好的起点。

- davidg