抽象解釈
プログラミング言語や仕様記述言語について、抽象解釈は抽象関係でリンクされたいくつかの意味論を与える。意味論とは、プログラムの振る舞いについての数学的説明である。プログラムの実際の実行に非常に近い、最も正確な意味論を concrete semantics(具体的意味論)と呼ぶ。例えば命令型言語の concrete semantics は、各プログラムが生成する実行トレースのようなものである。実行トレースはプログラム実行時の一連の状態であり、状態はプログラムカウンタの値とメモリの内容(広域変数、スタック、ヒープなど)からなる。より抽象化された意味論はそこから抽出される。例えば、実行時に到達可能な状態の集合だけを考慮する意味論が考えられる。
静的解析の目標は、いくつかの点で計算可能な意味解釈を抽出することである。例えば、整数の変数を具体的な値ではなくその符号(正、負、ゼロ)だけで表すことでプログラムの状態を表す。乗算などの基本演算について、このような抽象化では精度は失われない。積の符号を知るには、引数の符号がわかれば十分である。他の演算については、この抽象化で精度を失う可能性がある。例えば、引数が正と負の2つであった場合、その和の符号を知ることはできない。
精度を失うことは、意味論を決定可能にするのに必須な場合もある(ライスの定理とチューリングマシンの停止問題参照)。一般に、解析の精度とその決定性(計算可能性理論)や tractability(計算複雑性理論)はトレードオフの関係にある。
実際に定義される抽象は、解析したいプログラムの属性と対象プログラム群に合わせて調整される。
すると、f′(x′) ≤ x′ であるような x′ は f の最小不動点の抽象化である。
ここで問題となるのは、そのような x′ を求める方法である。L′ の高さが有限であるか、少なくとも昇鎖条件(全ての昇順は最終的に定常である)があるなら、そのような x′ は帰納によって次のように定義された昇順 x′n の定常の限界値として得られる。
x′0=⊥ (L′ の極小な元)
x′n+1=f′(x′n)
それ以外のケースでも、widening operator ∇ を通して、そのような x′ を得ることが可能である。これは、全ての x と y について x ∇ y が x と y のどちらよりも大きいか等しいという演算である。ここで全ての順序 y′n について、次のように定義される順序は最終的に定常的である。
x′0=⊥
x′n+1=x′n ∇ y′n
従って、y′n=f(x′n) となる。
場合によっては、ガロア接続(Galois connection)(α, γ) を使って抽象化を定義できる。ここで、αは L から L′ への関数、γは L′ から L への関数である。これは、必ずしも存在するとは限らない最良の抽象化の存在を前提としている。例えば、実数の組 (x,y) の集合を凸多面体で囲むことで抽象化する場合、x+y ≤ 1 で定義される円板の最良の抽象化は存在しない。