拡張静的チェック

拡張静的チェック( ESC ) は、コンピュータサイエンスにおいて、さまざまなプログラム制約の正しさを静的にチェックする一連の手法の総称です。 ^{[1] ESC は、}型チェックの拡張形式と考えることができます。型チェックと同様に、ESC はコンパイル時に自動的に実行されます(つまり、人間の介入なし)。この点で、ESC は、通常、人間が生成した証明に依存する、ソフトウェアの形式検証に対するより一般的なアプローチと区別されます。さらに、ESC は、偽陽性(実際のエラーではない過大評価されたエラー、つまり、厳密さよりも ESC)の数を大幅に削減することを目的としている点で、健全性よりも実用性を重視しますが、その代わりに、偽陰性(実際の ESC 過小評価エラーだが、プログラマが注意を払う必要がない、または ESC の対象ではない) が発生します。^{[2] [3] ESC は、}ゼロ除算、配列の範囲外、整数オーバーフロー、およびnull 参照など、現在型チェッカーの範囲外となっている一連のエラーを識別できます。

拡張静的チェックで使用される技術は、静的プログラム解析、シンボリックシミュレーション、モデルチェック、抽象解釈、SAT解決、自動定理証明および型チェックなど、コンピュータサイエンスのさまざまな分野から来ています。拡張静的チェックは、大規模なプログラムに拡張できるように、通常、プロシージャ間レベルではなくプロシージャ内レベルでのみ実行されます。^{[2]さらに、拡張静的チェックは、}事前条件と事後条件、ループ不変条件、クラス不変条件の形でユーザーが提供する仕様を活用してエラーを報告することを目的としています。

拡張静的チェッカーは通常、メソッドを通じて、前提条件 (それぞれ事後条件) から始まる最も強い事後条件(それぞれ最も弱い前提条件) を手続き内で伝播することによって動作します。このプロセス中の各ポイントで、そのプログラム ポイントでわかっていることをキャプチャする中間条件が生成されます。これは、そのポイントでのプログラム ステートメントの必要条件と組み合わされて、検証条件を形成します。この例として、除算を含むステートメントが挙げられます。その必要条件は、除数がゼロ以外であることです。このことから生じる検証条件は、実質的に、この時点での中間条件が与えられると、除数がゼロ以外になるはずです。メソッドが拡張静的チェックに合格するには (または「これ以上のエラーが見つかりません」)、すべての検証条件が偽 (したがって、除外された 3 番目によって正しい) であることが示されなければなりません。通常、何らかの形式の自動定理証明器を使用して検証条件を満たします。

^{拡張静的チェックは、ESC/Modula-3 [4]}で初めて導入され、その後ESC/Javaでも導入されました。そのルーツは、静的デバッグ^[5]やlint、FindBugsなどのより単純な静的チェック手法に由来しています。Spec #、 SPARKada、VHDL VSPECなど、他の多くの言語でもESCが採用されています。ただし、現在、基本開発環境で拡張静的チェックを提供するソフトウェアプログラミング言語は広く普及していません。

• Java モデリング言語(JML)

• Cormac Flanagan、K. Rustan M. Leino、Mark Lillibridge、Greg Nelson、James B. Saxe、Raymie Stata (2002)。「Java の拡張静的チェック」。プログラミング言語の設計と実装に関する ACM SIGPLAN 2002 会議の議事録。p. 234。doi : 10.1145/512529.512558。ISBN 978-1581134636. S2CID  47141042。{{cite book}}: CS1 maint: 複数の名前: 著者リスト (リンク)
• Babic, Domagoj; Hu, Alan J. (2008)。「Calysto」。第 13 回国際ソフトウェア工学会議の議事録 - ICSE '08。p. 211。doi : 10.1145 / 1368088.1368118。ISBN 9781605580791. S2CID  62868643。
• Chess, BV (2002)。「拡張静的チェックを使用したコンピュータセキュリティの向上」。2002 IEEE セキュリティおよびプライバシー シンポジウム議事録。pp. 160–173。CiteSeerX 10.1.1.15.2090。doi :  10.1109 / SECPRI.2002.1004369。ISBN 978-0-7695-1543-4. S2CID  12067758。
• Rioux, Frédéric; Chalin, Patrice (2006). 「拡張された静的チェックによる Web ベースのエンタープライズ アプリケーションの品質向上: ケース スタディ」.理論計算機科学の電子ノート. 157 (2): 119–132. doi : 10.1016/j.entcs.2005.12.050 . ISSN  1571-0661.
• James, Perry R .; Chalin, Patrice ( 2009). 「Java モデリング言語のより高速でより完全な拡張静的チェック」。Journal  of Automated Reasoning。44 ( 1–2): 145–174。CiteSeerX 10.1.1.165.7920。doi : 10.1007 /s10817-009-9134-9。ISSN 0168-7433。S2CID 14996225  。 
• Xu, Dana N. (2006). 「Haskell の拡張静的チェック」。2006 ACM SIGPLAN Haskell ワークショップの議事録。p. 48。CiteSeerX 10.1.1.377.3777。doi :  10.1145 / 1159842.1159849。ISBN 978-1595934895.S2CID 1340468  。
• Leino, K. Rustan M. (2001)。「拡張静的チェック: 10 年の展望」。情報科学。コンピュータ サイエンスの講義ノート。第 2000 巻。pp. 157–175。doi : 10.1007 /3-540-44577-3_11。ISBN 978-3-540-41635-7。
• Detlefs, David L.; Leino, K. Rustan M.; Nelson, Greg; Saxe, James B. (1998). 「拡張静的チェック」。Compaq SRC 調査レポート(159)。