著者

大熊 浩示 南出 靖彦

出版者

一般社団法人情報処理学会

雑誌

情報処理学会論文誌. プログラミング (ISSN:03875806)

巻号頁・発行日

vol.46, no.6, 2005-04-15

---

正しいコンパイラを得るためには, コンパイラの形式化が正しいだけでなく, その実装の正しさも検証しなければならない.我々は定理証明システムIsabelle/HOLを用いてコンパイラを形式化し, その正しさを検証した.さらに, Isabelle/HOLのコード生成機能を用い, Isabelle/HOLで記述されたコンパイラを実行可能なプログラムへ変換した.このコード生成機能はIsabelle/HOLの構文をStandard MLの構文に単純に変換するもので, 生成されたプログラムの信頼性は高いといえる.コンパイラは構文解析を除くすべてのフェーズがIsabelle/HOLで記述されており, コード生成機能で変換されたプログラムに構文解析プログラムなどを加えることにより実行可能な検証されたコンパイラを得ることができる.コンパイラはScheme構文を持つ関数型プログラミング言語を入力とし, Java仮想機械のアセンブリ言語を生成する.今回形式化したコンパイラはクロージャ変換やインライン展開など, これまで検証されたコンパイラでは扱われていない高度なプログラム変換を行っている.また, コンパイラの記述ではコンパイル時間も考慮し, 効率の良いデータ構造を採用した.得られたコンパイラをいくつかのSchemeプログラムに対して適用した結果, コンパイル時間, 生成されたプログラムの実行時間ともに既存のコンパイラに劣らない結果が得られた.