| 研究概要 |
近年,プログラム解析の最も有望な手法の一つとして型理論に基づく手法が注目されている.本研究では,プログラム解析のための型理論の構築・検証(すなわち解析手法の正しさの証明)を統一的に行うための枠組みを構築し,さらにそれに基づき,構成的プログラミングの考え方を用いて解析器の自動抽出を行う手法の確立を目指している.本年度の研究成果は以下の通り.
1.プログラム解析のための統一的型理論の拡張・改良
種々のプログラム解析を統一的に扱うための型システムとして,これまで研究してきたメモリやファィル,ネットワークなど計算機資源へのアクセス方法を統一的に解析するための型システムの拡張,改良を行った.また,統一的型システムのさらなる拡張の必要性を探るため,これまでの理論では扱えない,順序付き線形型システムについて研究を行い,プログラム変換への応用を示した.
2.型理論に基づくプログラム解析器の抽出実験
正しいプログラム解析器を自動抽出するためめ実験として,昨年に引き続き,一部をパラメータ化した汎用的型システムライブラリの定理証明支援器Coq上での定式化を続けるとともに,その上に単純型付きラムダ計算の定式化をおこなって,汎用ライブラリの有効性を確かめた.
3.並行計算モデルの定理証明器上での定式化
並行プログラムのための統一的型システムの定式化の前準備として,並行計算モデルであるπ計算の構文および操作的意味,仕様を記述するためのプロセス論理のCoq上での定式化を昨年度に引き続き行った.
|
