如何證明時/在伊莎貝爾/ HOL

Question

我有這樣的C代碼：

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

我想證明，無論列表有多長，當這個循環結束，p->next等於NULL，並EIP指的是這個循環之後的下一條指令。

但我不能。有沒有人知道如何證明在Isabelle/HOL？

Answer 1

一套工具（免責聲明：我是後者的作者），允許您將C代碼導入Isabelle/HOL，以進一步推理Michael Norrish的C Parser和AutoCorres。使用命令

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

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

到伊莎貝爾：

使用AutoCorres，我可以分析下面的C文件

theory List 
imports AutoCorres 
begin 

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

然後，我們可以證明，霍爾三重其中指出，對於任何輸入狀態，函數的返回值將爲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 

T他是一個部分正確性定理，其中有點陳述你所要求的。 （特別是，它指出如果功能終止，而如果它沒有錯，那麼後置條件爲真）。

爲了更完整的證明，你將需要一些更多的東西添加到上面：

1. 你需要知道的是，名單是有效的;例如，中間節點不指向無效地址（例如，未對齊的地址），並且該列表不構成循環（意味着while循環將永不終止）。

2. 您還需要證明終止。這與上面的第二個條件有關，但您可能仍然需要爲什麼它是真實的進行爭論。 （一種典型的方法是說列表的長度總是減少，因此循環最終會終止）。

AutoCorres沒有指示指令指針的概念（通常這些概念只存在於彙編級別），但終止的證明是類似的。

AutoCorres在DataStructures.thy中提供了推理鏈接列表的一些基本庫，這將是一個很好的起點。