静的コード解析
静的コード解析 (せいてきコードかいせき、static code analysis) または静的プログラム解析 (static program analysis) とは、コンピュータのソフトウェアの解析手法の一種であり、実行ファイルを実行することなく解析を行うこと。逆にソフトウェアを実行して行う解析を動的プログラム解析と呼ぶ。静的コード解析はソースコードに対して行われることが多いが、少数ながらオブジェクトコードに対して行う場合もある。また、この用語は以下に列挙するツールを使用した解析を意味することが多い。人間が行う作業はインスペクション、コードレビューなどと呼ぶ。日本語では静的コード分析とも訳される。
WSDL validator (Eclipse)
Parasoft SOAtest (商用)
形式手法は、ソフトウェアやハードウェアの解析に用いられる用語であり、厳密に数学的な手法によって解析結果を得ることを意味する。数学的手法としては、表示的意味論、公理的意味論、操作的意味論、抽象解釈などがある。
実行時エラーを全て検出することは不可能であることが証明されており、任意のプログラムが正しく動作するかエラーになるかを判定する機械的手法はない。これは1930年代のアラン・チューリングやライスの研究で判明した(チューリングマシンの停止問題およびライスの定理)。決定不能な問題ではあるが、近似的な解でも有効である。
形式的な静的コード解析の実装方法には以下のようなものがある:
モデル検査は、有限の状態を持つシステムを対象とし、無限に状態を持つシステムを抽象化によって状態数を有限個に減らして行うこともある。
データフロー解析は、プログラムの各点で変数群の取りうる値についての情報を集める技法である。
抽象解釈は、プログラムの個々の文が抽象機械の状態に何らかの影響を与える様子をモデル化したものである(つまり、ソフトウェアを個々の文の数学的属性と宣言に基づいて「実行」する)。抽象機械は解析しやすいようになるべく単純化されるので、実際のプログラムを完全に表すわけではない(もとのシステムで真である属性が抽象システムで常に真とは限らない)。うまくいけば、抽象解釈は「健全」とされる(抽象システムで真である全属性はもとのシステムでも真だといえる)。例えば、Frama-cやPolyspaceといったツールは、抽象解釈の技法を使っている。
表明をプログラム内で使うことは、ホーア論理で最初に示唆された。一部のプログラミング言語は表明をツールとしてサポートしている。