誰かがZ3自体でZ3を証明しようとしましたか？
Z3を使用して、Z3が正しいことを証明することさえ可能ですか？
より理論的には、X自体を使用して、ツールXが正しいことを証明することは可能ですか？
2225 次
2 に答える
29
簡単に言えば、「いいえ、誰も Z3 自体を使用して Z3 を証明しようとはしませんでした」:-)
「プログラム X が正しいことを証明した」という文は、非常に誤解を招きます。主な問題は、正しいとはどういう意味かということです。Z3 の場合、少なくとも、充足不可能な問題に対して「sat」を返さず、充足可能な問題に対して「unsat」を返さない場合、Z3 は正しいと言えます。この定義は、次のような追加のプロパティを含めることで改善される場合があります。Z3 はクラッシュしない。Z3 API の関数 X にはプロパティ Y などがあります。
何を証明する必要があるかについて合意した後、ランタイムのモデル、プログラミング言語のセマンティクス (Z3 の場合は C++) などを作成する必要があります。次に、ツール (検証ツール) を使用して、実際のコードを次のコードに変換します。 Z3 などの定理証明器を使用してチェックする必要がある式のセット。Z3 は C++ を「理解」しないため、ベリファイアが必要です。Verifying C Compiler ( VCC ) は、この種のツールの例です。このアプローチを使用して Z3 が正しいことを証明しても、Z3 が本当に正しいという決定的な保証は得られないことに注意してください。これは、モデルが正しくない、検証者が正しくない、Z3 が正しくないなどの可能性があるためです。
VCC などの検証ツールを使用するには、検証したいプロパティ、ループ不変条件などでプログラムに注釈を付ける必要があります。いくつかの注釈は、コード フラグメントが何をすべきかを指定するために使用されます。他の注釈は、定理証明者を「助ける/導く」ために使用されます。場合によっては、注釈の量が検証対象のプログラムよりも多くなります。したがって、プロセスは完全に自動化されていません。
もう 1 つの問題はコストです。このプロセスには非常にコストがかかります。Z3 を実装するよりもはるかに時間がかかります。Z3 には 30 万行のコードがあり、このコードの一部は非常に微妙なアルゴリズムと実装のトリックに基づいています。もう 1 つの問題はメンテナンスです。定期的に新しい機能を追加し、パフォーマンスを改善しています。これらの変更は証明に影響します。
コストは非常に高くなる可能性がありますが、VCC は、Microsoft Hyper-V ハイパーバイザーなどの重要なコードを検証するために使用されてきました。
理論的には、プログラミング言語 X の検証ツールは、それが言語 X でも実装されていれば、それ自体を証明するために使用できます。Spec#検証ツールはそのようなツールの例です。Spec# は Spec# に実装されており、Spec# のいくつかの部分は Spec# を使用して検証されました。Spec# は Z3 を使用しており、それが正しいと想定していることに注意してください。もちろん、これは大前提です。
これらの問題と Z3 アプリケーションの詳細については、次の論文を参照してください: http://research.microsoft.com/en-us/um/people/leonardo/ijcar10.pdf
于 2011-08-03T15:47:16.747 に答える
2
いいえ、ツール自体を使用して、重要なツールが正しいことを証明することはできません。これは基本的に、ゲーデルの第 2 不完全性定理で述べられています。
基本的な算術的真理と、形式的証明可能性に関する特定の真理を含む正式な効果的に生成された理論 T について、T がそれ自体の一貫性のあるステートメントを含む場合、T は矛盾しています。
Z3 には算術演算が含まれているため、それ自体の一貫性を証明することはできません。
上記のコメントで言及されているため: ユーザーが不変条件を提供しても、ゲーデルスの定理は適用されます。これは計算可能性の問題ではありません。定理は、そのような証明は一貫したシステムには存在できないと述べています。
ただし、Z3 を使用して Z3 の一部を検証することはできます。
5年後に編集：
実際、この議論はゲーデルの不完全性定理よりも簡単です。
満たされない数式に対してのみ UNSAT を返す場合、Z3 が正しいとしましょう。
A が満たされない場合、Z3 が正しいような式 A を見つけたとします (そして、この関係は何らかの形で証明されています)。
この式を Z3 に与えることができますが、
- Z3 が UNSAT を返す場合、Z3 が正しいか、Z3 のバグが原因である可能性があります。したがって、何も確認していません。
- Z3 が SAT とカウンターモデルを返す場合、モデルを分析することで Z3 のバグを見つけることができるかもしれません
- そうでなければ、私たちは何も知りません。
したがって、Z3 を使用して Z3 のバグを見つけ、Z3 に関する信頼を (非常に高いレベルまで) 向上させることができますが、正式に検証することはできません。
于 2013-11-23T13:46:27.567 に答える