4

単純なプロパティや定理を示すために、OCaml での使用例を探しています。一例として、二分木の ocaml 定義が与えられた場合、ノードの最大数が 2^(h+1)-1 であることを示します。

二分木とグラフのそのような種類の例を見つけましたが、他には何もありません..提案やリンクはありますか?

4

1 に答える 1

14

紙に書かれた証明について話している場合、使用法は本質的に他の言語の場合と同じです。つまり、プログラムのセマンティクスの合理的な (ただし形式化されていない) モデルに基づく非公式の推論です。あなたのケースを処理するために、私は 2 つの関数sizeとを書き、2 つのサブツリーの帰納仮説を使用してheight、ツリーの帰納的推論によって証明します。size h <= pow 2 (height h + 1) - 1

より正式な証明が必要な場合は、いくつかの方法があります。

  • hoare ロジックに基づく証明手法は、関数型プログラミング言語に適用されています。たとえば、Régis-Gianas と Pottier の 2008 年の作品、A Hoare logic for call-by-value functions を参照してください。それらは、あなたの主張のより厳密な (現実的であるため) 証明を与えるために、まだ手書きの証明で使用できるものの正式な基礎を提供します。定理証明にも使用できますが、このアプローチがまだ完全に解決されているかどうかはわかりません。

  • もう 1 つの自然なアプローチは、 Coq証明アシスタントで直接プログラムを作成することです。Coq証明アシスタントのプログラミング言語は、ほとんどが OCaml の純粋に機能的なサブセットであり、その機能を証明に使用します。これは OCaml での記述とまったく同じではありませんが、かなり似ています。次に、OCaml の実装を直接ミラーリングするか、Coq の抽出機能を使用して、Coq プログラムから「コンパイル」された見た目の良い OCaml コードを取得します。このアプローチは、OCaml 標準ライブラリに存在するバランスの取れたバイナリ ツリーの実装を形式化するために使用されており、2 つの実装 (OCaml のものと Coq のもの) は十分に同期されているため、結果を転送して OCaml 側の変更が正しいことを証明できます。 .

  • 同様に、一部のドメインでは、Coq などの一般的な定理証明よりも便利な認定プログラミング用の言語を設計する試みがいくつかあります。なぜ3はそのような「ソフトウェア検証プラットフォーム」です: プログラミング言語 (OCaml からそう遠くない) とその上に仕様言語を定義します。プログラムに関するアサーションを定式化し、一般的な証明アシスタント (Coq など) やより自動化された定理証明器 (SMT ソルバー) などのさまざまな手法を使用してそれらを検証できます。Why3 は、従来の命令型スタイルのアルゴリズム実装の検証をサポートするよう努めていますが、関数型プログラミング スタイルもサポートしているため、完全な Coq に行きたくない場合 (たとえば、アルゴリズムの確実な終了には関心がないため、Coq では不便な場合があります)。

  • 最後に、次のテクニックに関する作業が行われました: OCaml プログラムを読み取り、それから「Coq 記述」を自動的に生成します。これにより、正しいと証明されたことが OCaml 実装でも保持されるという保証とともにプロパティを設定できます。これは、Arthur Charguéraud の 2010 年の博士論文の主な結果であり、「Coq 記述」は「特性式」の手法に基づいています。彼は、Union-Find などの比較的洗練されたアルゴリズムの正しい ML 実装や、Chris Okasaki の優れた本「Purely Functional Data Structures」からの例を証明することができました。

(私はよく Coq 証明アシスタントについて言及します。Isabelle や Agda などの他のツールも同様に適していますが、Coq は構文が OCaml 言語に近いため、ML プログラムを再実装して正式に証明する場合は、おそらく良い選択です。正しい。）

于 2012-10-18T08:18:54.510 に答える