|
本研究では、プログラム解析のための型理論の構築・検証(すなわち解析手法の正しさの証明)を統一的に行うための枠組みを構築し、さらにそれに基づき、構成的プログラミングの考え方を用いて解析器の自動抽出を行う手法の確立を目指している.本年度の研究成果は以下の通り.
1.プログラム解析のための統一型理論の拡張・改良
種々のプログラム解析を統一的に扱うための型システムとして、これまで研究してきた計算機資源使用法解析および並行プログラムの解析を拡張するとともに、並行プログラム解析器TyPiCalを実装し、そのソースプログラムをホームページ上で公開した.
2.型理論に基づくプログラム解析器の抽出実験
正しいプログラム解析器を自動抽出するための実験として、昨年に引き続き、一部をパラメータ化した汎用的型システムライブラリの定理証明支援器Coq上での定式化を行い、その上に単純型付きラムダ計算の定式化を行って汎用ライブラリの有効性を確かめた.昨年度に比べ、準同型写像を使ったライブラリ部分の拡充を行うなどしてライブラリの完成度を高めた.
3.並行プログラムの検証のためのCoq用ライブラリの構築
並行プログラムを定理証明器上で検証するためのCoq用ライブラリの作成を行った.今後は上記1番目の項目の並行プログラムの型に基づく解析の定式化を本ライブラリに組み込んでいく予定である.
|
