要約解釈

コンピュータ科学において、抽象解釈とは、順序集合、特に格子上の単調関数に基づいて、コンピュータプログラムの意味論を的確に近似する理論である。これは、すべての計算を実行することなく、その意味論（例えば、制御フロー、データフロー）に関する情報を得る、コンピュータプログラムの部分的な実行と見なすことができる。

その主な具体的な応用例は形式静的解析であり、コンピュータプログラムの可能な実行に関する情報を自動的に抽出するものである。このような解析には主に2つの用途がある。

• コンパイラ内部で、プログラムを解析して、特定の最適化や変換が適用可能かどうかを判断する。
• デバッグのため、あるいはプログラムのバグの種類に対する検証のため。

抽象解釈は、 1970年代後半にフランスのコンピュータ科学者夫婦であるパトリック・クーゾーとラディア・クーゾーによって形式化された。 ^{[ 1 ] [ 2 ]}

このセクションでは、現実世界の非コンピュータ的な例を用いて、抽象的解釈を解説します。

会議室にいる人たちを考えてみましょう。部屋にいる一人ひとりに、アメリカの社会保障番号のような固有の識別子が割り当てられているとします。誰かが出席していないことを証明するには、その人の社会保障番号がリストに載っていないかどうかを確認するだけで済みます。二人の異なる人が同じ番号を持つことはあり得ないので、番号を調べるだけで参加者の出席の有無を証明または否定することが可能です。

しかし、出席者の名前だけが登録されている可能性もあります。リストに名前が見つからない場合は、その人は出席していなかったと安全に結論付けることができますが、名前が見つかった場合は、同音異義語の可能性（例えば、ジョン・スミスという名前の人が2人いる場合）があるため、さらなる調査なしには断定できません。同音異義語は実際にはまれであるため、この不正確な情報でもほとんどの目的には十分であることに注意してください。ただし、厳密に言えば、誰かが部屋にいたと断言することはできません。言えるのは、その人がそこにいた可能性があるということだけです。調べている人物が犯罪者であれば、警報を発令しますが、もちろん誤報を発令する可能性もあります。同様の現象は、プログラムの分析でも発生します。

もし私たちが特定の情報、例えば「成人がいたかどうか」だけに興味がある場合${\displaystyle n}$部屋にいる全員の名前と生年月日のリストを作成する必要はありません。参加者の年齢のリストを作成するだけで十分であり、正確さを損なうことはありません。それでもまだ扱いきれない場合は、最年少の年齢だけを記録しておけばよいでしょう。${\displaystyle m}$そして最年長者、${\displaystyle M}$質問が厳密に以下の年齢に関するものである場合${\displaystyle m}$または厳密には${\displaystyle M}$そうすれば、そのような参加者はいなかったと安全に答えることができるでしょう。そうでなければ、分からないとしか言​​えないかもしれません。

計算においては、一般的に、具体的で正確な情報は有限の時間とメモリ内では計算できません（ライスの定理と停止問題を参照）。抽象化は、質問に対する一般的な回答を可能にするために用いられます（例えば、抽象解釈アルゴリズムが正確な回答を確実に計算できない場合に、「はい」または「いいえ」を意味するはい／いいえの質問に対して「たぶん」と答えるなど）。これにより問題が単純化され、自動的な解決が可能になります。重要な要件の一つは、問題が扱いやすくなるように十分な曖昧さを加えつつ、重要な質問（例えば、「プログラムがクラッシュする可能性はあるか？」）に答えるのに十分な精度を維持することです。

プログラミング言語または仕様記述言語が与えられた場合、抽象解釈とは、抽象化関係によって結び付けられた複数の意味論を与えることである。意味論とは、プログラムの可能な動作を数学的に特徴づけたものである。プログラムの実際の実行を非常に正確に記述する最も精密な意味論は、具体意味論と呼ばれる。例えば、命令型プログラミング言語の具体意味論は、各プログラムに対して、そのプログラムが生成する実行トレースの集合を関連付けることができる。実行トレースとは、プログラムの実行における連続する状態のシーケンスであり、状態は通常、プログラムカウンタの値とメモリ位置（グローバル変数、スタック、ヒープ）で構成される。さらに抽象的な意味論が導き出される。例えば、実行において到達可能な状態の集合のみを考慮することができる（これは、有限トレースにおける最後の状態を考慮することに相当する）。

静的解析の目的は、ある時点で計算可能な意味解釈を導き出すことです。例えば、整数変数を操作するプログラムの状態を、変数の実際の値を忘れて符号（+、−、または0）だけを保持することで表現することができます。乗算などの基本的な演算では、このような抽象化によって精度が失われることはありません。積の符号を得るには、被演算の符号を知っていれば十分です。しかし、他の演算では、抽象化によって精度が失われる場合があります。例えば、被演算がそれぞれ正と負である和の符号を知ることは不可能です。

意味論を決定可能にするためには、精度を多少犠牲にする必要がある場合がある（ライスの定理や停止問題を参照）。一般に、解析の精度と決定可能性（計算可能性）、あるいは扱いやすさ（計算コスト）の間には妥協点が存在する。

実際には、定義される抽象化は、分析したいプログラムの特性と、対象となるプログラムのセットの両方に合わせて調整されます。抽象解釈によるコンピュータプログラムの最初の大規模な自動分析は、 1996年のアリアン5ロケットの初飛行の失敗につながった事故がきっかけとなりました。 ^{[ 3 ]}

させて${\displaystyle L}$を順序集合（具体集合と呼ばれる）とし、${\displaystyle L'}$は、抽象集合と呼ばれる別の順序集合である。これら2つの集合は、一方の集合の要素を他方の集合に写像する全関数を定義することによって互いに関連付けられている。

関数${\displaystyle \alpha }$要素をマッピングする場合、それは抽象化関数と呼ばれます。${\displaystyle x}$コンクリートセット${\displaystyle L}$要素へ${\displaystyle \alpha (x)}$抽象セットにおいて${\displaystyle L'}$つまり、要素 ${\displaystyle \alpha (x)}$で${\displaystyle L'}$は抽象化である${\displaystyle x}$で${\displaystyle L}$。

関数${\displaystyle \gamma }$要素をマッピングする場合、それは具体化関数と呼ばれます。${\displaystyle x'}$抽象セットにおいて${\displaystyle L'}$要素へ${\displaystyle \gamma (x')}$コンクリートセット${\displaystyle L}$つまり、要素${\displaystyle \gamma (x')}$で${\displaystyle L}$は具体化である${\displaystyle x'}$で${\displaystyle L'}$。

させて${\displaystyle L_{1}}$、${\displaystyle L_{2}}$、${\displaystyle L'_{1}}$、 そして${\displaystyle L'_{2}}$順序付けられた集合である。具体的な意味論${\displaystyle f}$は単調関数である${\displaystyle L_{1}}$に${\displaystyle L_{2}}$関数${\displaystyle f'}$から${\displaystyle L'_{1}}$に${\displaystyle L'_{2}}$は有効な抽象化であると言われている${\displaystyle f}$もし、すべての${\displaystyle x'}$で${\displaystyle L'_{1}}$、 我々は持っています${\displaystyle (f\circ \gamma )(x')\leq (\gamma \circ f')(x')}$。

プログラムの意味論は、ループや再帰手続きが存在する場合、一般的に固定点を使用して記述されます。${\displaystyle L}$は完全な格子であり、${\displaystyle f}$単調関数である${\displaystyle L}$の中へ${\displaystyle L}$それで、${\displaystyle x'}$そのため${\displaystyle f(x')\leq x'}$は最小不動点の抽象化である${\displaystyle f}$これは、クナスター・タルスキの定理によれば存在する。

問題は、${\displaystyle x'}$。 もし${\displaystyle L'}$有限の高さを持つか、少なくとも上昇連鎖条件（すべての上昇数列は最終的に定常状態になる）を満たすならば、そのような${\displaystyle x'}$上昇数列の定常極限として得られる可能性がある${\displaystyle x'_{n}}$帰納法によって以下のように定義される。${\displaystyle x'_{0}=\bot }$（最小要素${\displaystyle L'}$） そして${\displaystyle x'_{n+1}=f'(x'_{n})}$。

他のケースでは、そのような${\displaystyle x'}$（ペア）拡大演算子を介して、^{[ 4 ]}二項演算子として定義される${\displaystyle \nabla \colon L\times L\to L}$以下の条件を満たすもの：

1. すべての人にとって${\displaystyle x}$そして${\displaystyle y}$、 我々は持っています${\displaystyle x\leq x\mathbin {\nabla } y}$そして${\displaystyle y\leq x\mathbin {\nabla } y}$、 そして
2. 任意の昇順数列${\displaystyle (y'_{n})_{n\geq 0}}$定義されるシーケンス${\displaystyle x'_{0}:=\bot }$そして${\displaystyle x'_{n+1}:=x'_{n}\mathbin {\nabla } y'_{n}}$は最終的には静止している。${\displaystyle y'_{n}=f'(x'_{n})}$。

場合によっては、ガロア接続を用いて抽象化を定義することが可能です。${\displaystyle (\alpha ,\gamma )}$どこ${\displaystyle \alpha }$から${\displaystyle L}$に${\displaystyle L'}$そして${\displaystyle \gamma }$から${\displaystyle L'}$に${\displaystyle L}$これは最良の抽象化の存在を前提としているが、必ずしもそうとは限らない。例えば、カップルの集合を抽象化すると、${\displaystyle (x,y)}$凸多面体を囲むことによって実数を表す場合、円盤への最適な抽象化は存在しない。${\displaystyle x^{2}+y^{2}\leq 1}$。

• モデル検査
• 記号シミュレーション
• 象徴的な処刑
• 静的コード解析ツール一覧―抽象解釈に基づく（健全な）ツールとアドホックな（不健全な）ツールの両方を含む
• 静的プログラム解析―解析手法の概要（抽象解釈を含むが、これに限定されない）
• インタープリタ（コンピュータ）

• パトリック・クーゾーが管理する抽象解釈に関するウェブページ
• ロベルト・バニャーラの論文は、C言語に似たプログラミング言語に対して抽象解釈に基づく静的解析器を実装する方法を示している。
• 静的解析シンポジウムの論文集は、Springer LNCSシリーズに掲載されています。
• POPL会議に付随する検証、モデル検査、および抽象解釈に関する会議（VMCAI）の議事録は、Springer LNCSシリーズに掲載される。

講義ノート

• 抽象解釈。パトリック・クーゾー。MIT。
• デイビッド・シュミットによる抽象解釈に関する講義ノート
• モラーとシュヴァルツバッハによる静的プログラム解析に関する講義ノート
• アゴスティーノ・コルテージによるプログラム解析と検証に関する講義ノート
• グレゴワール・シュトルによるスライドでは、抽象解釈の各ステップを多くの例を交えて解説し、ガロアとの関連性も紹介しています。