c - Isabelle/HOL で while/for を証明する方法

Question

私はこのCコードを持っています:

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

リストがどんなに長くても、このループが終わったら にp->next等しくNULL、EIP はこのループの次の命令を参照することを証明したいのです。

しかし、私はできません。Isabelle/HOLでループを証明する方法を知っている人はいますか?

Answer 1

さらに推論するために C コードを Isabelle/HOL にインポートできるツールのセット (免責事項: 私は後者の作成者です) は、Michael Norrish のC Parser and 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. また、終了を証明する必要があります。これは上記の 2 番目の条件に関連していますが、それが真である理由について議論する必要があるでしょう。（典型的な方法は、リストの長さが常に減少するため、ループは最終的に終了すると言うことです）。

AutoCorres は命令ポインターの概念を指示しませんが (通常、これらの概念はアセンブリ レベルでのみ存在します)、終了の証明は同様です。

AutoCorres は、リンクされたリストについて推論するためのいくつかの基本的なライブラリを提供していますDataStructures.thy。