ソフトウェアにおける形式的検証の全体像

Question

私は正式なソフトウェア検証の状態の全体像をまとめようとしているのですが、かなり苦労しています。文脈を説明すると、私は主に数学の出身です。私は、整形式の数学的ステートメント (例:Coq、Isabelle、Leanなど）。私が理解するのに苦労しているのは、実際の CS アプリケーションにおける「形式的手法」で何が起こっているのかということです。

Microsoft や AWS などの企業が、ソフトウェア開発の「正式な手法」として TLA+ をある程度実質的に使用していることがわかりました。しかし、ウェインの本を読み始めたとき、 実践的な TLA+ 本を読んだところ、彼は、たとえば長さのリストのソートアルゴリズムをチェックするだけであれば、プログラムは正式にチェックされるべきであると考えていたことがわかりました。 $<n$ 1 と 2 の間のエントリ $n$ いくつかの修正済み $n$, 、つまり私たちは有限個のケースをチェックしているだけであり、したがってアルゴリズムは一般的に機能するはずであると言っているだけです。これは特に興味深いものではないようです。これは特に厳密な単体テストの一例にすぎません。特に、これは正しさの正式な証明ではありません。

その一方で、イザベルとコックは数学の定理を証明できるのと同じように、ソフトウェアに関することも証明できるというつぶやきを見たことがあります。しかし、これを約束しているように見える本を調べてみると、たとえば、クリパラさん 依存型を使用した認定プログラミング, プログラムの正式な検証に漠然と関連していると思われる抽象的な内容を多く見かけますが、広く使用されている言語で書かれた実際のプログラムを取り上げた例はありません (例:C++、Python、Java など)、または単に擬似コードを作成して「検証」するだけでも、それが意味するものは何でも構いません。

誰か私の混乱を解消してもらえませんか？

Answer 1

正式に証明されたプログラムは、言語に関係なく、正式に証明されたプログラムです。プログラムが Coq で書かれているという理由だけで、おそらく 抽出された C++ や Java などの「エンタープライズ」言語で書かれたものではなく、OCaml や Haskell に置き換えられたからといって、プログラムに劣るわけではありません。

汎用プログラミング言語で書かれたプログラムを証明するのは、たとえ Haskell のような「おとなしい」言語であっても、困難です。なぜなら、これらの言語には通常、多くの便利な機能、パフォーマンスやオペレーティング システムとのインターフェースのための暗い部分、豊富で複雑なライブラリが含まれているからです。プログラムのプロパティを証明するには、まずこのプロパティを記述する必要があります。このステートメントには、プログラムが記述されている言語のセマンティクスが埋め込まれます。最初に正式な意味論を持たずに設計された言語 (ほぼすべての言語がこれに当てはまります) を形式化しようとすると、すぐに英語の説明で未指定のままになったり、曖昧になったり、完全に自己矛盾したりする暗い部分に突き当たることになります。リファレンス実装が説明どおりに動作しない場合、それは実装ではなく英語のバグとみなされます。既存の言語で書かれたプログラムのプロパティを証明する最新技術は、プログラムをその言語のサブセットに制限することです。

そのサブセットに何が含まれるかは非常に多様です。糖衣構文はそれほど難しくありません。セマンティクスはそれをより単純な構造に変換するだけで済みます。リフレクション プロパティはモデル化するのが特に難しいわけではありませんが、モデルを推論するのがはるかに難しくなる可能性があります (たとえば、「このコード スニペットにはこの変数を参照する方法がないため、この変数を参照することはできません」などのプロパティが無効になります)値を変更する」)ため、多くのフレームワークがこれを除外しています。オペレーティング システムとの対話 (通常はライブラリ経由) には、オペレーティング システムのモデリングが必要であり、非常に複雑になるため、問題が発生します。浮動小数点演算は、連続する演算全体で近似値を追跡し続けると大きな爆発を引き起こすため、困難です。

C の場合、正式なモデルを備えた主要な大規模サブセットの 1 つは CompCert C です。 コンプサート. 。CompCert は正式に検証されたコンパイラ (Coq で書かれている) であるため、C プログラムのプロパティを証明すると、生成されたマシン コードの証明も追加で取得できます。 コンプサート C は C99 の非常に大きなサブセットですが、形式化により標準ライブラリの大部分と言語のいくつかの癖が除外されます。

現実世界のプログラミング言語 (の適切なサブセット) で書かれたプログラムを証明するには、証明を扱いやすいようにプログラムを構造化する必要があります。実際には、これは、最初に高水準言語 (実際のハードウェアには実装されていない) でプログラムを作成して証明し、この高水準言語を最終プログラムの仕様として使用することを意味します。多くの場合、実行可能プログラムと仕様の間には、いくつかのレベルの連続した改良が存在します。

最終的なプログラムが手動で書かれるのではなく、高水準言語から機械的に抽出されるのがかなり一般的です。例えばOCamlに抽出したCoqを書いたり、 F* C に抽出されます。しかし、逆のアプローチも可能です。たとえば、C を (「飼い慣らして」) 書き、それに関数のプロパティや他のコード部分の注釈を付けて、次のようにすることもできます。 フレームC これらの特性 (および C プログラムには未定義の動作がないという暗黙の特性) を証明するためです。

プログラミング言語の形式的意味論とプログラムのプロパティを表現する方法がある場合、これらのプロパティを証明することは数学の定理です。通常、これらの定理には微積分のような複雑な数学は含まれません (物理的オブジェクトの動きの追跡など、アプリケーション領域で持ち込まれる場合を除く) が、非常に大規模な式が含まれ、算術ステートメントが含まれるため、証明するのが困難です。 ($x^n+y^n=z^n$ は複雑な方程式ではありませんが、それを解くことは初歩的なものではありません!)。その すべてのプログラムの重要な意味論的特性を証明できるプログラムを書くことは理論的に不可能, そして、典型的なプログラムの多くの興味深い特性を証明できるプログラムを書くことは事実上不可能です。形式的検証には、問題を十分に小さなステップに分割すること (小さな関数を記述し、それらの関数の十分に正確なプロパティを記述する) と、それらのプロパティの一部 (たとえば、 SATソルバー 命題論理の場合）、コンピューターができない証明を人間に書かせる（ただし、コンピューターは人間の証明をチェックします）。Coq や Isabelle などの証明アシスタントがこの最後のステップに参加します。

現実世界のプログラムを正式に証明するのは大変な労力であり、一般的なソフトウェア プロジェクトよりもはるかに多くの時間と専門知識が必要です。高保証環境以外で実行されることはほとんどありません。ほとんどの場合、交通機関 (飛行機、電車、車はそれほど多くありません) などの安全要件が高い環境、スペースなどのコストが高い環境、または (非常にまれに) スマート デバイスなどの高いセキュリティ要件がある環境で行われます。カード。

たとえば、ある固定 n に対して 1 から n までのエントリを持つ長さ <n のリストに対するソート アルゴリズムを確認するとします。私たちは有限個のケースをチェックしているだけであり、したがってアルゴリズムは一般的に機能するはずであると言っているだけです。

プログラムの入力項目が n 項目に制限されていない限り、これは正式な証明にはなりません。私はこの本を知りませんが、あなたが何かを読み間違えたのではないかと思います。ソート プログラムを正式にチェックするには、すべての n についてその正しさを証明する必要があります。