コンピュータプログラムの抽象解釈
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/06/23 10:02 UTC 版)
「抽象解釈」の記事における「コンピュータプログラムの抽象解釈」の解説
プログラミング言語や仕様記述言語について、抽象解釈は抽象関係でリンクされたいくつかの意味論を与える。意味論とは、プログラムの振る舞いについての数学的説明である。プログラムの実際の実行に非常に近い、最も正確な意味論を concrete semantics（具体的意味論）と呼ぶ。例えば命令型言語の concrete semantics は、各プログラムが生成する実行トレースのようなものである。実行トレースはプログラム実行時の一連の状態であり、状態はプログラムカウンタの値とメモリの内容（広域変数、スタック、ヒープなど）からなる。より抽象化された意味論はそこから抽出される。例えば、実行時に到達可能な状態の集合だけを考慮する意味論が考えられる。 静的解析の目標は、いくつかの点で計算可能な意味解釈を抽出することである。例えば、整数の変数を具体的な値ではなくその符号（正、負、ゼロ）だけで表すことでプログラムの状態を表す。乗算などの基本演算について、このような抽象化では精度は失われない。積の符号を知るには、引数の符号がわかれば十分である。他の演算については、この抽象化で精度を失う可能性がある。例えば、引数が正と負の2つであった場合、その和の符号を知ることはできない。 精度を失うことは、意味論を決定可能にするのに必須な場合もある（ライスの定理とチューリングマシンの停止問題参照）。一般に、解析の精度とその決定性（計算可能性理論）や tractability（計算複雑性理論）はトレードオフの関係にある。 実際に定義される抽象は、解析したいプログラムの属性と対象プログラム群に合わせて調整される。
※この「コンピュータプログラムの抽象解釈」の解説は、「抽象解釈」の解説の一部です。
「コンピュータプログラムの抽象解釈」を含む「抽象解釈」の記事については、「抽象解釈」の概要を参照ください。
- コンピュータプログラムの抽象解釈のページへのリンク
