最近、私は正式な検証について多くのことを読んでいて、このトピックに魅了されています。しかし、私は次のことを理解できません:
正式な検証には正式な仕様が必要ですが、プログラムの正式な仕様がない場合、コンパイラのソース コードでどのように抽象的な解釈を使用できますか?
正しいと思われる外国語のテキストからの翻訳 (また、正式な仕様は必要ないようです)。
プログラムがその制御フロー チャートによって表される場合、各分岐はプログラムの状態を表し (複数の場合があります。たとえば、ループでは分岐が複数回通過します)、抽象的な解釈により、この状態のセットに近似する静的セマンティクスが作成されます。
正式な検証手法としての抽象的な解釈に関する記事: http://www.di.ens.fr/~cousot/publications.www/Cousot-NFM2012.pdf
言語仕様マニュアルに従って結果を計算する言語のインタープリターを構築することにより、「具体的な解釈」を行うことができます。(言語マニュアルが非公式であるという事実は、そのような通訳者の正しさを永久に疑うものです)。
抽象解釈に必要なのは、プログラムのセマンティクスをよく理解していることと、抽象化する価値があるものについての考えだけです。これは、上記のインタープリターを使用して、実際の計算を計算の抽象化に置き換えることで取得できます。たとえば、すべての整数値を「正」、「ゼロ」、「負」、または「不明」として表すことができます。これでまだ計算でき、定性的な結果が得られます。さらに重要なことは、実際のプログラム入力 (おそらく単に抽象化された値) を必要とせずに、これを使用して計算できることです。抽象インタープリターは形式的な意味でも完全に信頼できないことに注意してください。なぜなら、言語が何をするかについてのガイドとして非公式のリファレンスマニュアルを使用して計算しているためです。
さて、このような抽象プログラムを実行すると、null 値を制御する変数が「未定義」ではないという誤り (たとえば、null 値の逆参照) を発見するかもしれません。その場合、プログラムにバグがあることを示唆できます。あなたは正しくないかもしれませんが、これにより有用な結果が得られる可能性があります。
非公式のリファレンス マニュアルをまだ使用しているため、実際の抽象的な解釈では、プログラムが正式に計算する内容はどこにもわかりません。マニュアルが正式なドキュメントになり、抽象的なインタプリタが証明可能な正しい手順から派生した場合、プログラムの抽象的な解釈は、プログラムが実際に行うことの抽象化を法とする一種の仕様であることに同意するかもしれません。
抽象的な解釈が、プログラムの意図の正式な仕様へのアクセスを提供する場所はどこにもありません。したがって、仕様に関してプログラムが「正しい」ことを証明するためにそれを単独で使用することはできません。