コンパイラの正確性

コンピューティングにおいて、コンパイラの正確性は、コンパイラが言語仕様に従って動作することを示すことを目的とするコンピュータサイエンスの分野です。^{[要出典]手法には、}形式手法を 使用してコンパイラを開発することや、既存のコンパイラに対して厳密なテスト (コンパイラ検証と呼ばれることが多い) を使用することが含まれます。

コンパイルの正確性を確立するための2 つの主な形式検証アプローチは、すべての入力に対するコンパイラの正確性を証明することと、特定のプログラムのコンパイルの正確性を証明すること (翻訳検証) です。

形式手法によるコンパイラ検証には、長い一連の形式的演繹論理が含まれます。^[1] しかし、証明を見つけるためのツール（定理証明器）はソフトウェアで実装されており、複雑なため、エラーが含まれる可能性が高くなります。1つのアプローチは、証明を検証するツール（証明チェッカー）を使用することです。これは、証明ファインダーよりもはるかに単純なため、エラーが含まれる可能性が低くなります。

このアプローチの顕著な例はCompCertであり、これはC99の大規模なサブセットの形式検証された最適化コンパイラである。^{[2] [3] [4]}

^{CakeMLプロジェクト[5]}では、別の検証済みコンパイラが開発され、HOL（証明支援システム）を使用して標準MLプログラミング言語 のかなりのサブセットの正しさを確立しました。

形式的に正しいコンパイラを得るためのもう一つのアプローチは、セマンティクス指向のコンパイラ生成を使用することである。^[6]

コンパイラがすべての有効な入力プログラムに対して正しいことを証明しようとするのとは対照的に、翻訳検証 ^[7] は、与えられた入力プログラムが正しくコンパイルされたことを自動的に確立することを目指しています。与えられたプログラムの正しいコンパイルを証明することは、コンパイラがすべてのプログラムに対して正しいことを証明するよりも潜在的に簡単ですが、固定されたプログラムは依然として任意の大きな入力で動作し、任意の長い時間実行される可能性があるため、依然として記号推論が必要です。翻訳検証は、与えられたコンパイルに対してコンパイルが正しかったことの証明を生成することにより、既存のコンパイラ実装を再利用できます。翻訳検証は、与えられたプログラムに対してこの誤りが明らかにならない限り、時々誤ったコードを生成するコンパイラでも使用できます。入力プログラムによっては、翻訳検証が失敗することがあります (生成されたコードが間違っているか、翻訳検証手法が正しさを示すには弱すぎるため)。ただし、翻訳検証が成功した場合、コンパイルされたプログラムはすべての入力に対して正しいことが保証されます。

テストはコンパイラの出荷における作業のかなりの部分を占めるが、標準的な文献では比較的あまり取り上げられていない。1986 年版のAho、Sethi、Ullman には、コンパイラのテストに関する 1 ページのセクションがあるが、具体的な例は示されていない。^[8] 2006 年版ではテストのセクションが省略されているが、その重要性は強調されている。「最適化コンパイラを正しく動作させることは非常に難しいため、完全にエラーのない最適化コンパイラは存在しないと言っても過言ではない。したがって、コンパイラを書く上で最も重要な目的は、それが正しいことである。」^{[9] Fraser と Hanson 1995 には}、回帰テスト に関する短いセクションがあり、ソース コードが利用可能である。^[10] Bailey と Davidson 2003 では、プロシージャ呼び出しのテストについて取り上げている。 ^[11] 多くのリリースされたコンパイラには、重大なコード正当性のバグがあることを多くの記事が確認している。^[12] Sheridan 2007 は、一般的なコンパイラ テストに関する最新のジャーナル記事であると思われる。^[13]ほとんどの場合、コンパイラテストに関して入手可能な最大の情報は、Fortran ^[14]とCobol ^[15]の検証スイートです。

コンパイラをテストする際によく使われる手法としては、ファジング^[16]（コンパイラのバグを見つけるためにランダムなプログラムを生成する）やテストケース削減（見つかったテストケースを最小化して理解しやすくする）などがあります。^[17]

• コンパイラ
• 検証と検証（ソフトウェア）
• 正確性（コンピュータサイエンス）
• CompCert C コンパイラ— 形式検証済みの C コンパイラ
• 信頼を信頼することについての考察