Rubyプログラムの制御フロー解析とその健全性の証明

概要

論文の詳細を見る
Rubyプログラムの制御フロー解析を設計し,その健全性を操作的意味論に基づき証明する.Ruby などのスクリプト言語に関する静的プログラム解析は多く提案されているが,その健全性について言語の意味論に基づき証明がなされたものは少ない.本研究では,Ruby のコア言語について操作的意味論を定義し,その意味論に基づき制御フロー解析の健全性を証明する.Ruby のコア言語は,ruby 1.9 処理系の構文解析器によって得られる中間言語をモデルとし,メソッドの動的な定義・イテレータブロック・大域脱出などを含む.Ruby では,クラス・メソッドの定義は,宣言ではなく動的に評価される式であり,さらにメソッド定義の上書きが可能である.そのため,プログラムの実行時の制御フローによって,異なるクラス定義・メソッド定義が得られる可能性がある.本研究では,メソッド定義が評価されたかどうかについて,制御フローを区別する解析を行う.これにより,特に多く見られる,トップレベルでクラス・メソッドの定義を行うプログラムについては,メソッド呼び出しの正確な解析が可能となる.
2010-03-16