意味関数によるC言語の意味形式化

概要

論文の詳細を見る
プログラムの表示的意味論は、1969年D.Scottoらにより提案された。表示的意味論では、意味関数によってプログラムを意味領域上に写像し、そのプログラムの意味を意味領域上で関数として表現する。この意味領域上の関数を調べることにより計算の可能性、停止性を調べることが、さらには、プログラムの検証、意味同値性、デバッグ、自動合成等に応用可能となった。表示的意味論は、言語処理系の設計、実装にも応用でき、最近は、意味の設定から言語の設計がなされている。表示的意味論は、既存のプログラム言語の意味解釈にも使用されており、その解釈は、プログラムの高速化、コンパイラ製作の簡略化に役立っている。しかし、既存の言語に意味が定義された研究結果は多数あるが、ポインタに関する議論は十分されていない。ポインタは、マシン、OSへの依存度が高いため、抽象化が難しいと考えられているからである。ポインタをサポートするC言語に対して意味を設定することは、Cプログラムの計算可能性の判断や、自動生成、他言語との変換必要不可欠であると思われる。そこで本稿では、従来の研究ではなされていなかったポインタや構造体に関する意味記述に特に焦点をしぼり、C言語に対する意味関数の設定を行った。
一般社団法人情報処理学会の論文
1994-09-20

意味関数によるC言語の意味形式化

スポンサーリンク

概要

著者

関連論文

スポンサーリンク