| 研究概要 |
近年,プログラム解析の最も有望な手法の一つとして型理論に基づく手法が注目されている.本研究では,プログラム解析のための型理論の構築・検証(すなわち解析手法の正しさの証明)を統一的に行うための枠組みを構築し,さらにそれに基づき,構成的プログラミングの考え方を用いて解析器の自動抽出を行う手法の確立を目指している.本年度の研究成果は以下の通り.
1.プログラム解析のための統一的型理論の拡張・改良
種々のプログラム解析を統一的に扱うための型システムとしてこれまで研究してきた,(1)メモリやファイル,ネットワークなど計算機資源へのアクセス方法を統一的に解析するための型システム,(2)並行プログラムにおけるさまざまな通信・同期の整合性を統一的に解析するための型システムの改良を行い,より広い範囲のプログラム解析を扱えるようにした.具体的には,前者については,time regionと呼ぶ新しい概念を導入することにより,Javaバイトコードにおけるオブジェクトの初期化の解析なども統一的に扱えるようになった.
2.型理論に基づくプログラム解析器の抽出実験
正しいプログラム解析器を自動抽出するための実験として,ラムダ計算の(1)単純型システム,および(2)細部をパラメータ化した汎用的型システムを定理証明支援器Coq上で定式化し,Coqのプログラム抽出機能を用いてプログラム解析器(型推論器)の抽出実験を行った.
3.並行計算モデルの定理証明器上での定式化
並行プログラムのための統一的型システムの定式化の前準備として,並行計算モデルであるπ計算の構文および操作的意味,仕様を記述するためのプロセス論理の定式化をCoq上で行った.
|
