実行可能なコンパイラの形式化と検証
スポンサーリンク
概要
- 論文の詳細を見る
正しいコンパイラを得るためには, コンパイラの形式化が正しいだけでなく, その実装の正しさも検証しなければならない.我々は定理証明システムIsabelle/HOLを用いてコンパイラを形式化し, その正しさを検証した.さらに, Isabelle/HOLのコード生成機能を用い, Isabelle/HOLで記述されたコンパイラを実行可能なプログラムへ変換した.このコード生成機能はIsabelle/HOLの構文をStandard MLの構文に単純に変換するもので, 生成されたプログラムの信頼性は高いといえる.コンパイラは構文解析を除くすべてのフェーズがIsabelle/HOLで記述されており, コード生成機能で変換されたプログラムに構文解析プログラムなどを加えることにより実行可能な検証されたコンパイラを得ることができる.コンパイラはScheme構文を持つ関数型プログラミング言語を入力とし, Java仮想機械のアセンブリ言語を生成する.今回形式化したコンパイラはクロージャ変換やインライン展開など, これまで検証されたコンパイラでは扱われていない高度なプログラム変換を行っている.また, コンパイラの記述ではコンパイル時間も考慮し, 効率の良いデータ構造を採用した.得られたコンパイラをいくつかのSchemeプログラムに対して適用した結果, コンパイル時間, 生成されたプログラムの実行時間ともに既存のコンパイラに劣らない結果が得られた.
- 一般社団法人情報処理学会の論文
- 2005-04-15
著者
関連論文
- Rubyプログラムの制御フロー解析とその健全性の証明
- 特集「プログラミング及びプログラミング言語」の編集にあたって(プログラミング及びプログラミング言語)
- 実行可能なコンパイラの形式化と検証
- 実行可能なコンパイラの形式化と検証
- 実行可能なコンパイラの形式化と検証
- 「情報処理学会論文誌 : プログラミング」の編集について
- 多相レコード型に基づくRubyプログラムの型推論
- Cプログラムの検証ツールCaduceus(ソフトウェア紹介)
- POPL '96会議報告
- アトミックグループで拡張された正規表現のオートマトンへの変換
- 参照カウントに対応したソフトウェアトランザクショナルメモリの実装