gpt4 book ai didi

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

转载 作者:太空狗 更新时间:2023-10-29 15:52:28 26 4
gpt4 key购买 nike

我有这个 C 代码:

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

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

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

最佳答案

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

关于c - 如何在 Isabelle/HOL 中证明 while/for,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/19782243/

26 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com