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

【问题标题】：How to prove while/for in Isabelle/HOL如何在 Isabelle/HOL 中证明 while/for
【发布时间】：2013-11-15 22:17:27
【问题描述】：

我有这个 C 代码：

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

我想证明，不管列表有多长，当这个循环结束时，p->next等于NULL，EIP指的是这个循环之后的下一条指令。

但我不能。有谁知道如何在 Isabelle/HOL 中证明循环？

【问题讨论】：

我不知道有任何直接方法可以证明 Isabelle/HOL 中 C 代码的属性。您能否详细说明您正在尝试实现的目标以及您在哪里使用（或期望使用）这样做？也许afp.sourceforge.net/entries/Simpl.shtml 很有趣。顺便说一句：什么是“EIP”？
独立于您要使用的证明工具。您打算如何处理列表是循环的（即循环不终止）的情况？
你好@chris。对不起，我不能告诉你太多细节，这是一个团队工作，还没有发布。我可以告诉你的是，我们在 Isabelle 中模拟 X86 ISA 指令，比如 mov、jmp。 gcc 生成的汇编代码被翻译成 Isabelle，并在 Isabelle 中运行。当没有循环时，结果非常好。但是我们不能处理循环，这要困难得多。我们想证明对于所有 n，这个 while 循环将以 p->next 等于 NULL 结束，并且 eip (pc) 将指向循环下面的下一条指令。
我不是在询问您项目的细节；），只是更多的上下文，例如，您使用的是 Isabelle 的哪个逻辑，如何将 C 代码导入 Isabelle，...没有这个，你的问题不容易回答。

标签： c loops while-loop isabelle

【解决方案1】：

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

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

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

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

使用命令进入伊莎贝尔：

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

这是一个部分正确性定理，它有点说明了你的要求。（特别是，它声明 if 函数终止，并且 if 它没有出错，那么后置条件为真。

要获得更完整的证明，您需要在上面添加一些内容：

你需要知道列表是有效的；例如，中间节点不指向无效地址（例如，未对齐的地址），并且列表不形成循环（意味着 while 循环永远不会终止）。
您还需要证明终止。这与上面的第二个条件有关，但您可能仍需要就它为什么为真提出一个论据。（一种典型的方法是说列表的长度总是减少，因此循环最终会终止）。

AutoCorres 不指导指令指针的概念（通常这些概念仅存在于汇编级别），但终止证明将是类似的。

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

【讨论】：