実際のフォーマルプログラム検証

いくつかの質問に簡潔に回答しようと思います。これは厳密には私の研究分野ではないため、一部の情報が古くなっている/正しくない可能性があることに注意してください。

1. プロパティを正式に証明するために特別に設計されたツールが多数あります。 JavaとC ++の。

   ただし、ここで少し余談をする必要があります。プログラムの正当性を証明するとはどういう意味ですか？ Java型チェッカーは、Javaプログラムの正式なプロパティを証明します。つまり、floatやintの追加などの特定のエラーは決して発生しません。発生する！プログラムが望ましくない状態になることは決してない、または特定の関数の出力が特定の数学的仕様に準拠しているという、はるかに強力なプロパティに関心があると思います。つまり、単純なセキュリティプロパティから、プログラムが詳細な仕様を満たしていることの完全な証明まで、「プログラムが正しいことを証明する」とは、さまざまな意味があります。

   ここで、次のことを想定します。プログラムに関する強力なプロパティを証明することに関心があります。セキュリティプロパティに関心がある場合（プログラムが特定の状態に到達できない ）、一般的にはモデル検査。ただし、Javaプログラムの動作を完全に指定する場合は、その言語の仕様言語（ JML 。たとえば、 ACSL など、Cプログラムの動作を指定するための言語がありますが、私にはわかりません。 C ++。

2. 仕様を取得したら、プログラムがその仕様に準拠していることを証明する必要があります。

   このためには、両方の正式な理解妥当性定理を表現するための、仕様と言語（JavaまたはC ++）の操作的意味論、つまり実行プログラムのは仕様を尊重します。

   このツールを使用すると、その定理の証明を定式化または生成することもできます。現在、これらのタスク（指定と証明）はどちらも非常に難しいため、多くの場合、2つに分けられます。

   • コード、仕様を解析し、妥当性定理を生成する1つのツール。フランクが述べたように、クラカトアはそのようなツールの例です。

   • 定理を証明する1つのツール（ s）、自動的またはインタラクティブに。 Coqはこの方法でKrakatoaと対話し、 Z3 のような強力な自動化ツールもいくつか使用できます。

   1つの（マイナーな）ポイント：自動化された方法で証明するには難しすぎる定理がいくつかあり、自動定理証明者には、信頼性を低下させる健全性のバグがあることが知られています。これは、Coqが比較して優れている領域です（ただし、自動ではありません）。

3. Ocamlコードを生成する場合は、必ず最初にCoq（Gallina）で記述してください。次に、コードを抽出します。ただし、Coqは、可能であれば、C ++またはJavaの生成にひどいです。

4. 上記のツールはスレッド化とパフォーマンスの問題を処理できますか？おそらくそうではないでしょう。パフォーマンスとスレッドの問題は、特に難しい問題であるため、特別に設計されたツールによって最も適切に処理されます。 MartinHofmannの PolyNI プロジェクトは興味深いようですが、ここで推奨するツールがあるかどうかはわかりません。

結論：「実世界」のJavaおよびC ++プログラムのフォーマル検証は、大規模で十分に開発された分野であり、Coqはそのタスクの一部に適しています。たとえば、概要はここにあります。

コメント

• この投稿と追加した参照に感謝します。 IMHO、ソフトウェアエンジニアの目標は、1）常に正しい結果を提供し、2）失敗しないシステムを迅速にリリースできるようにすることです。ここでリグレッションの問題が発生する可能性があります。ここでは、仕様自体が”バグフリー” :-)のようなものであることを証明する必要があります。 “言語の真の提案”をメタ言語で定義しようとし、そのために別のメタ言語が必要になり、次に別の言語が必要になるようなものです。 1つ…
• 問題は、ユーザー”が望んでいること”が通常正式に表現されていないことです。言語！通常、この質問に対する正式な回答はありません：”この正式な仕様は私の非公式の考えに準拠していますか？”。 ‘形式仕様をテストして、特定の数学的特性があることを証明することは可能ですが、最終的には数学を実世界に関連付ける必要があります。これは非公式のプロセスです。
• もちろんです。正式な方法は、明確に定義されたポイントからしか開始できないことに常に気づきました。その仕様が実際のユーザーの意識的/無意識的/未発見のニーズに準拠しているかどうかは別の問題であり、形式手法では対処できません（ただし、エンジニアにとっては確かに問題です）。
• 定理は定義上提案を証明した。したがって、おそらく”定理を証明するつもりはありません”。
• @nbroWikipediaは同意しているようですあなたと。ただし、Mathworldは、定理を、受け入れられている数学演算によって” 真であると証明できる命題であると定義しています”。この場合、定理の証明を与えることは可能であるだけでなく、それらをそれと呼ぶことを正当化するために必要です！ ：）（もちろん、これは反論です）

3つの注目すべきアプリケーションについて言及したいと思います。業界または重要な実際のシステムにおける形式手法/形式検証ツールの例。私はこのトピックに関する経験がほとんどなく、論文を読むことからしか学んでいないことに注意してください。

1. オープンソースツール Java Pathfinder （略してJPF） 2005年にNASAによってリリースされたは、実行可能なJavaバイトコードプログラムを検証するシステムです（ Java Pathfinder @ wiki ）。これは、NASAエイムズのK9ローバーのエグゼクティブソフトウェアの不整合を検出するために使用されています。

2. このペーパー：モデル検査を使用した重大なファイルシステムエラーの検出@ OSDI “04 は、使用方法を示しています。ファイルシステムの重大なエラーを見つけるためのモデル検査。FiSCと呼ばれるシステムが、広く使用され、十分にテストされた3つのファイルシステム（ext3、JFS、ReiserFS）に適用され、32の重大なバグが見つかりました。BestPaperAwardを受賞しました。

3. このペーパー：Amazon WebServicesが正式なメソッドを使用する方法@CACM “15 では、AWSが正式なメソッドをS3、DynamoDB、EBS、内部分散ロックマネージャーなどの製品。 LamportのTLA + ツールに焦点を当てています。ちなみに、Lamportは独自のTLAツールボックスを集中的に使用しています。彼はTLAで（かなり完全な）フォーマル検証を行うことがよくあります。論文の付録で彼自身（および共著者）によって提案されたアルゴリズム/定理の一覧。

安全性が重要な組み込みシステム用に設計されたC ++のサブセットで記述されたプログラムでフォーマル検証が可能になりました。 http://eschertech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.pptを参照してください。短いプレゼンテーションの場合は、フルペーパーの場合は http://eschertech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.pdf 。

コメント

• リンクをありがとう。特にリンクが企業のWebサイトへのリンクであるため、リンクの腐敗を防ぐために、少なくともコンテンツの簡単な概要が役立ちます。それらは定期的に再編成され、サイトへのすべてのリンクが削除される傾向があります。

フォーマルプログラムの仕様は、（多かれ少なかれ）別のプログラミング言語で書かれたプログラムです。その結果、仕様には確かに独自のバグが含まれます。

フォーマル検証の利点は、プログラムと仕様が2つの別個の実装であるため、バグが異なることです。しかし、常にではありません。バグの一般的な原因の1つである見落とされたケースは、しばしば一致します。したがって、フォーマル検証は万能薬ではありません。それでも、重要な数のバグを見逃す可能性があります。

フォーマル検証の欠点は、実装コストの2倍、おそらくそれ以上のコストがかかる可能性があることです（必要なフォーマル仕様のスペシャリストであり、それに付属する多かれ少なかれ実験的なツールを使用する必要があります。それは安くはありません。

テストケースとそれらを実行するための足場を設定すると思います。自動的に時間を有効に活用できます。

コメント

• フォーマル検証の利点は… 。フォーマル検証の2番目のデメリットは…これは混乱を招きます。
• 仕様と非公式タスクの不一致は、プログラミングの問題ではなく、ソフトウェア要件分析の問題だと思います。

いくつかの異なる質問をします。私は、産業/商業アプリケーションのフォーマル検証方法がそれほど一般的ではないように見えることに同意します。ただし、プログラムの正当性を判断するために、コンパイラには多くの「フォーマル検証」の原則が組み込まれていることを理解する必要があります。したがって、ある意味で、最新のコンパイラを使用する場合は、「フォーマル検証で最先端の技術の多くを使用しています。

「テストにうんざりしている」と言いますが、フォーマル検証実際にはテストの代わりにはなりません。ある意味で、テストのバリエーションです。

Javaについて言及しています。 FindBugs と呼ばれるJava検証プログラムに組み込まれている多くの高度なフォーマル検証メソッドがあり、実際に大規模なコードベースで実行できます。 「誤検知と誤検知」の両方が発生するため、人間の開発者が結果を確認/分析する必要があることに注意してください。ただし、実際の機能上の欠陥が発生していなくても、通常はコードで回避する必要のある「アンチパターン」が発生することに注意してください。

特定のアプリケーションについては「産業用」以外は言及しません。 。実際のフォーマル検証は、特定のアプリケーションに依存する傾向があります。

フォーマル検証手法は、回路の正確さを証明するためにEEで広く使用されているようです。

これは、 Lars Philipson によるEE分野のフォーマル検証ツールの調査の例です。

コメント

• ‘と誤解を招く” a多くの”フォーマル検証”の原則がコンパイラに組み込まれており、プログラムの正確性を判断します”。あなたが参照しているのは、一部のコンパイラが行う静的な型チェックですが、その方法で検証されたプロパティはかなり単純です。数字と文字列の追加を避けます。これは役に立ちますが、”フォーマル検証”によって通常理解されていることとはかけ離れています。
• そうではありませんでした。静的型チェックを具体的に参照してください。ただし、これは単純で一般的な例の1つです。広く普及しているimhoコンパイラ最適化手法は、最適化されたプログラムバリアントの同等性を判断/表示する高度な手法を含むため、フォーマル検証の原則とほぼ同じです。したがって、ここで”ムービングゴールポスト”の問題を回避することが重要であるように思われ、コンパイラがそれを実行する、またはそのビルドを行うという理由だけで想定しないでくださいコンパイラに、それはフォーマル検証ではありません。
• これは一般的な理解ではないことに同意しました。最適化手法は、おおまかに言って、ループやサブルーチンなどのプログラム動作のモデルを作成し、そのモデルを最適化してから、おそらく同等の新しいコードを生成します。したがって、これらの最適化のいくつかは、コード&を再配置する際に非常に洗練されており、フォーマル検証の原則を利用しています。コンパイラのフォーマル検証方法には他にも多くの例があるようです…元の質問は多くの人が指摘しているように多くの異なる質問をしましたが、そこに含まれるすべての質問に答えようとはしていません。
• JRE、Javaランタイムエンジンなどでも使用されているフォーマル検証の原則があるようです…
• つまり” 記のfilmusで言及されているフォーマル検証”のi>夢は、キメラの抽象化であり、実用的/実用的/現実的な業界はそれをそのように広く認識しています。大規模なコードベースは、コードの$ y $ K行ごとに本質的に$ x $のバグ/欠陥があることが何十年も前から知られており、理論/テクノロジーがどのように進歩しても、これは決して変更されません。 i>人間の性質。実際、人間が作成した数学的定理は同じ特性を持っていますが、これは広く認められていません！

おそらく、モデルチェッカーが役立つかもしれません。

http://alloytools.org/documentation.html Alloyはモデルチェッカーです。

Alloyを使用したモデル検査の概念を説明する素晴らしいプレゼンテーション： https://www.youtube.com/watch?v=FvNRlE4E9QQ

同じファミリのツールに「プロパティベースのテスト」があり、それらはすべて、ソフトウェアの特定の仕様モデルの反例を見つけようとします。