抽象解釈
抽象解釈（Abstract Interpretation）は、コンピュータプログラムの意味論を健全に近似する理論です。順序集合（特に束）における単調関数に基づいており、プログラムの完全な実行をせずに、その振る舞いに関する情報を抽出できます。これは、プログラムの部分的な実行と見なすことができ、制御構造や情報の流れなど、プログラムの意味に関する重要な情報を得ることができます。
抽象解釈の主な応用は、形式的な静的コード解析です。静的コード解析は、プログラムを実行せずにその性質を分析する手法であり、抽象解釈を用いることで、プログラムの実行に関する情報を自動的に抽出できます。この情報は、主に以下の2つの目的で使用されます。
1. コンパイラ最適化: プログラムの解析結果に基づいて、コンパイラがプログラムを最適化したり、変換したりする際に利用されます。例えば、不要な処理を削除したり、より効率的なコードを生成したりするために使われます。
2. デバッグと検証: プログラムのバグを検出したり、特定の種類のバグが存在しないことを保証するために利用されます。例えば、メモリリークや配列外参照などのエラーを静的に検出することができます。
抽象解釈は、Patrick Cousot と Radhia Cousot によって定式化されました。
抽象解釈の概念を理解するために、コンピュータ以外の実世界の例を見てみましょう。
会議室に人が集まっている状況を考えます。ある人物がまだ来ていないことを確認したい場合、最も確実な方法は出席者の名前とID番号（例えば、社会保障番号）をリストアップすることです。ID番号は一意であるため、リストを参照すれば特定の人物が出席しているかどうかを正確に判断できます。
しかし、もし名前しかリストアップできない場合、少し複雑になります。もしある人物の名前がリストにない場合、その人物が来ていないことはほぼ確実です。しかし、もし名前があったとしても、その人物が確実にそこにいるとは言えません。なぜなら、同姓同名の別人である可能性があるからです。実際には同姓同名は稀ですが、このような不正確な情報でも多くの場合有用です。
例えば、「n歳の人物が部屋にいるか？」という質問に答えたい場合、出席者の名前と生年月日のリストは必要ありません。単に出席者の年齢のリストがあれば、正確に答えられます。もし、そのようなリストを作成するのが難しい場合は、出席者の最小年齢mと最大年齢Mだけを保持することもできます。もし質問の年齢nがmよりも小さいか、Mよりも大きい場合は、そのような人物がいないと断言できます。それ以外の場合は「わからない」としか答えられません。
コンピュータの場合、確実で正確な情報を有限の時間とメモリで計算することは一般的に不可能です。抽象化によって問題を単純化し、自動的に解けるレベルにします。重要なのは、抽象化によって精度を保ちつつ、問題を扱える程度にまで簡略化することです。
プログラミング言語や仕様記述言語において、抽象解釈は抽象関係で関連付けられた複数の意味論を提供します。意味論とは、プログラムの振る舞いを数学的に記述したものです。最も正確な意味論は「具体的意味論（concrete semantics）」と呼ばれ、プログラムの実際の実行に非常に近いものです。例えば、命令型言語の具体的意味論は、各プログラムが生成する実行トレース（プログラム実行時の一連の状態）です。
より抽象化された意味論は、具体的意味論から抽出されます。例えば、実行時に到達可能な状態の集合だけを考慮する意味論が考えられます。静的解析の目標は、計算可能な意味解釈を抽出することです。例えば、整数の変数を具体的な値ではなく、その符号（正、負、ゼロ）で表現することでプログラムの状態を表します。乗算のような基本演算では、このような抽象化でも精度は失われません。しかし、加算のような他の演算では、精度が失われる可能性があります。
抽象化によって精度を失うことは、意味論を決定可能にするために必要となる場合があります。一般に、解析の精度と決定性、および計算可能性の間にはトレードオフの関係があります。実際に定義される抽象は、解析したいプログラムの属性と対象プログラム群に合わせて調整されます。
Lを具体的集合（concrete set）、L'を抽象集合（abstract set）とし、これらは関数αとγで関連付けられます。
抽象化関数 (abstraction function) α: Lの要素xをL'の要素α(x)にマップします。α(x)はxの抽象化です。
具体化関数 (concretization function) γ: L'の要素x'をLの要素γ(x')にマップします。γ(x')はx'の具体化です。
具体的意味論fがL1からL2への単調関数であるとき、L'1からL'2への関数f'をfの妥当な抽象化と呼びます。これは、全てのx' ∈ L'1に対して、(f ∘ γ)(x') ≤ (γ ∘ f')(x')が成り立つことを意味します。
プログラム意味論は、一般的にループや再帰における不動点を使って表されます。Lが完備束であり、fがLからLへの単調関数である場合、f'(x') ≤ x'であるようなx'はfの最小不動点の抽象化です。
このようなx'を求める方法は、L'の高さが有限であるか、または昇鎖条件が満たされる場合には、次の漸化式で定義される昇順x'_nの定常限界として得られます。
x'_0 = ⊥ (L'の最小要素)
x'_{n+1} = f'(x'_n)
それ以外の場合は、widening operator ∇を使用してx'を得ることが可能です。これは、全てのxとyについて、x ∇ yがxとyの両方以上であるという演算です。
ガロア接続(Galois connection)(α, γ)を使って抽象化を定義できる場合もあります。これは、最良の抽象化が存在することを前提としています。しかし、必ずしも最良の抽象化が存在するとは限りません。
プログラムのある時点で、変数xに代入されている値の区間が[lx,hx]であるとします。この場合、値v(x)をxに代入することは、v(x)が[lx,hx]の区間にあることを意味します。変数xとyの区間がそれぞれ[lx,hx]と[ly,hy]の場合、x+yの区間は[lx+ly,hx+hy]、x-yの区間は[lx-hy,hx-ly]となります。これは「厳密な」抽象化であり、x+yの取りうる値の集合は、その区間と正確に対応しています。同様に、乗算や除算についても導出可能です。これを「区間演算」といいます。
しかし、以下の単純なプログラムを例として考えてみましょう。
y = x;
z = x - y;
算術的な計算ではzの値はゼロになるはずですが、区間演算を行うと、例えばxの区間が[0,1]の場合、zの区間は[-1,1]となってしまいます。これは、個々の演算は厳密に抽象化されているものの、それを合成した結果が厳密ではないことを示しています。これは、区間演算ではxとyの値が等しいという関係が無視されているためです。区間の領域では、変数間の関係は考慮されません。これを「非関係的領域（non-relational domain）」といいます。
非関係的領域は高速で実装が容易ですが、正確性に欠けます。変数間の関係を扱う抽象領域の例として、以下のようなものがあります。
凸多面体
八角形
差分境界行列
線形等式
これらの抽象領域は、より正確な解析を可能にする一方で、計算コストが高くなります。抽象領域を選択する際には、解析の精度と計算コストのバランスを考慮する必要があります。
抽象解釈を利用したツールとして以下のようなものがあります。
ASTRÉE
PolySpace Embedded Software Verification
PAG と PAG/WWW
Airac
Goanna
DAEDALUS
コードに対する通常の解釈
モデル検査
記号シミュレーション
David Schmidt's lecture notes on abstract interpretation
* Michael Schwarzbach's lecture notes on static analysis
抽象解釈の主な応用
抽象解釈の主な応用は、形式的な静的コード解析です。静的コード解析は、プログラムを実行せずにその性質を分析する手法であり、抽象解釈を用いることで、プログラムの実行に関する情報を自動的に抽出できます。この情報は、主に以下の2つの目的で使用されます。
1. コンパイラ最適化: プログラムの解析結果に基づいて、コンパイラがプログラムを最適化したり、変換したりする際に利用されます。例えば、不要な処理を削除したり、より効率的なコードを生成したりするために使われます。
2. デバッグと検証: プログラムのバグを検出したり、特定の種類のバグが存在しないことを保証するために利用されます。例えば、メモリリークや配列外参照などのエラーを静的に検出することができます。
抽象解釈は、Patrick Cousot と Radhia Cousot によって定式化されました。
直観的解説
抽象解釈の概念を理解するために、コンピュータ以外の実世界の例を見てみましょう。
会議室に人が集まっている状況を考えます。ある人物がまだ来ていないことを確認したい場合、最も確実な方法は出席者の名前とID番号（例えば、社会保障番号）をリストアップすることです。ID番号は一意であるため、リストを参照すれば特定の人物が出席しているかどうかを正確に判断できます。
しかし、もし名前しかリストアップできない場合、少し複雑になります。もしある人物の名前がリストにない場合、その人物が来ていないことはほぼ確実です。しかし、もし名前があったとしても、その人物が確実にそこにいるとは言えません。なぜなら、同姓同名の別人である可能性があるからです。実際には同姓同名は稀ですが、このような不正確な情報でも多くの場合有用です。
例えば、「n歳の人物が部屋にいるか？」という質問に答えたい場合、出席者の名前と生年月日のリストは必要ありません。単に出席者の年齢のリストがあれば、正確に答えられます。もし、そのようなリストを作成するのが難しい場合は、出席者の最小年齢mと最大年齢Mだけを保持することもできます。もし質問の年齢nがmよりも小さいか、Mよりも大きい場合は、そのような人物がいないと断言できます。それ以外の場合は「わからない」としか答えられません。
コンピュータの場合、確実で正確な情報を有限の時間とメモリで計算することは一般的に不可能です。抽象化によって問題を単純化し、自動的に解けるレベルにします。重要なのは、抽象化によって精度を保ちつつ、問題を扱える程度にまで簡略化することです。
コンピュータプログラムの抽象解釈
プログラミング言語や仕様記述言語において、抽象解釈は抽象関係で関連付けられた複数の意味論を提供します。意味論とは、プログラムの振る舞いを数学的に記述したものです。最も正確な意味論は「具体的意味論（concrete semantics）」と呼ばれ、プログラムの実際の実行に非常に近いものです。例えば、命令型言語の具体的意味論は、各プログラムが生成する実行トレース（プログラム実行時の一連の状態）です。
より抽象化された意味論は、具体的意味論から抽出されます。例えば、実行時に到達可能な状態の集合だけを考慮する意味論が考えられます。静的解析の目標は、計算可能な意味解釈を抽出することです。例えば、整数の変数を具体的な値ではなく、その符号（正、負、ゼロ）で表現することでプログラムの状態を表します。乗算のような基本演算では、このような抽象化でも精度は失われません。しかし、加算のような他の演算では、精度が失われる可能性があります。
抽象化によって精度を失うことは、意味論を決定可能にするために必要となる場合があります。一般に、解析の精度と決定性、および計算可能性の間にはトレードオフの関係があります。実際に定義される抽象は、解析したいプログラムの属性と対象プログラム群に合わせて調整されます。
形式的定義
Lを具体的集合（concrete set）、L'を抽象集合（abstract set）とし、これらは関数αとγで関連付けられます。
抽象化関数 (abstraction function) α: Lの要素xをL'の要素α(x)にマップします。α(x)はxの抽象化です。
具体化関数 (concretization function) γ: L'の要素x'をLの要素γ(x')にマップします。γ(x')はx'の具体化です。
具体的意味論fがL1からL2への単調関数であるとき、L'1からL'2への関数f'をfの妥当な抽象化と呼びます。これは、全てのx' ∈ L'1に対して、(f ∘ γ)(x') ≤ (γ ∘ f')(x')が成り立つことを意味します。
プログラム意味論は、一般的にループや再帰における不動点を使って表されます。Lが完備束であり、fがLからLへの単調関数である場合、f'(x') ≤ x'であるようなx'はfの最小不動点の抽象化です。
このようなx'を求める方法は、L'の高さが有限であるか、または昇鎖条件が満たされる場合には、次の漸化式で定義される昇順x'_nの定常限界として得られます。
x'_0 = ⊥ (L'の最小要素)
x'_{n+1} = f'(x'_n)
それ以外の場合は、widening operator ∇を使用してx'を得ることが可能です。これは、全てのxとyについて、x ∇ yがxとyの両方以上であるという演算です。
ガロア接続(Galois connection)(α, γ)を使って抽象化を定義できる場合もあります。これは、最良の抽象化が存在することを前提としています。しかし、必ずしも最良の抽象化が存在するとは限りません。
抽象領域の例
プログラムのある時点で、変数xに代入されている値の区間が[lx,hx]であるとします。この場合、値v(x)をxに代入することは、v(x)が[lx,hx]の区間にあることを意味します。変数xとyの区間がそれぞれ[lx,hx]と[ly,hy]の場合、x+yの区間は[lx+ly,hx+hy]、x-yの区間は[lx-hy,hx-ly]となります。これは「厳密な」抽象化であり、x+yの取りうる値の集合は、その区間と正確に対応しています。同様に、乗算や除算についても導出可能です。これを「区間演算」といいます。
しかし、以下の単純なプログラムを例として考えてみましょう。
y = x;
z = x - y;
算術的な計算ではzの値はゼロになるはずですが、区間演算を行うと、例えばxの区間が[0,1]の場合、zの区間は[-1,1]となってしまいます。これは、個々の演算は厳密に抽象化されているものの、それを合成した結果が厳密ではないことを示しています。これは、区間演算ではxとyの値が等しいという関係が無視されているためです。区間の領域では、変数間の関係は考慮されません。これを「非関係的領域（non-relational domain）」といいます。
非関係的領域は高速で実装が容易ですが、正確性に欠けます。変数間の関係を扱う抽象領域の例として、以下のようなものがあります。
凸多面体
八角形
差分境界行列
線形等式
これらの抽象領域は、より正確な解析を可能にする一方で、計算コストが高くなります。抽象領域を選択する際には、解析の精度と計算コストのバランスを考慮する必要があります。
ツール
抽象解釈を利用したツールとして以下のようなものがあります。
ASTRÉE
PolySpace Embedded Software Verification
PAG と PAG/WWW
Airac
Goanna
関連項目
DAEDALUS
コードに対する通常の解釈
モデル検査
記号シミュレーション
外部リンク
David Schmidt's lecture notes on abstract interpretation
* Michael Schwarzbach's lecture notes on static analysis
もう一度検索
【記事の利用について】
タイトルと記事文章は、記事のあるページにリンクを張っていただければ、無料で利用できます。
※画像は、利用できませんのでご注意ください。
【リンクついて】
リンクフリーです。