如何在Isabelle/HOL中证明/ for

Question

我有这个C代码:

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

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

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

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提供了一些基本库来推理链表DataStructures.thy,这将是一个很好的起点.