如何证明在伊莎贝尔/霍尔

Question

我有一个C代码：

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

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

但是我不能。有人知道如何证明伊莎贝尔/霍尔的循环吗？

Answer 1

一组工具(免责声明:我是后者的作者)允许您将C代码导入Isabelle/HOL以进行进一步的推理，这是Michael的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为在DataStructures.thy中进行链接列表的推理提供了一些基本库，这将是一个很好的起点。