Extended static checking とは

拡張静的検査(ESC)は、さまざまなプログラム制約の正確性を静的にチェックするためのさまざまな手法の総称です。 ESCは、タイプチェックの拡張形式と考えることができます。型チェックと同様に、ESCはコンパイル時に自動的に実行されます(人間の介入なし)。これは、一般的に人間が作成した証明に依存するソフトウェアの正式な検証に対するより一般的なアプローチとは区別されます。さらに、偽陽性(実際のエラーではない過大評価されたエラー、すなわち厳格さに対するESC)を劇的に減らすことを目指して、偽陰性(実際のESCの過小評価エラー、プログラマの注意を必要としない、またはESCの対象にしていない)。 ESCは、ゼロ除算、配列の範囲外、整数オーバーフロー、およびヌル逆参照を含む、現在タイプ・チェッカーの範囲外にあるエラーの範囲を識別できます。
拡張静的検査で使用される技術は、静的プログラム解析、記号シミュレーション、モデル検査、抽象解釈、SAT解法、自動定理証明、型チェックなど、コンピュータサイエンスのさまざまな分野に由来します。拡張静的検査は一般に、大規模なプログラムに拡大するために、プロシージャ内レベル(プロシージャ内ではなく)でのみ実行されます。さらに、拡張静的検査は、事前および事後条件、ループ不変量およびクラス不変量の形で、ユーザが指定した仕様を利用してエラーを報告することを目指しています。
拡張静的チェッカーは、通常、前提条件(後置条件)から開始するメソッドを使用して、最強の事後条件(最も弱い前提条件)を反復的に伝播することによって動作します。このプロセスの各ポイントで、そのプログラムポイントで既知のものを取得する中間条件が生成されます。これは、検証条件を形成するために、その時点でプログラム文の必要条件と組み合わされる。これの一例は除算を含むステートメントであり、必要条件は除数がゼロでないことである。このことから生じる検証条件は、この時点で中間条件が与えられれば、除数が非ゼロであることに従わなければならないことを効果的に述べている。すべての検証条件は、メソッドが拡張静的検査(または「エラーを見つけることができない」)に合格するためには、false(したがって、除外された第3の手段によって正しい)と示されなければならない。典型的には、自動化された定理証明者のある形式が、検証条件を放電するために使用される。
Extended Static Checkingは、ESC / Modula-3、そして後でESC / Javaで開発されました。その根は、静的なデバッグやLint(ソフトウェア)やFindBugsなどのより単純な静的検査テクニックから始まります。 Spec#、SPARKada、VHDL VSPECを含む他の多くの言語がESCを採用しています。しかし、現時点では、基本開発環境において拡張静的検査を提供する広く使用されているソフトウェアプログラミング言語は存在しない。