2010 Fiscal Year Annual Research Report
高階再帰スキームのモデル検査とそのプログラム検証への応用
| Project/Area Number |
10J03842
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
塚田 武志 東北大学, 大学院・情報科学研究科, 特別研究員(DC1)
|
|---|
| Keywords | 高階再帰スキーム / モデル検査 / プログラム検証 |
|---|
| Research Abstract |
本研究では,関数型プログラムを実行前に検証する技術の基礎理論である,型を用いた高階再帰スキームのモデル検査について研究している,本研究はより広い範囲のプログラムに対してより広い範囲の仕様を検証できるようにすることを目指している.本年度の成果は以下の通り.1.プッシュダウンオートマトンで記述できる仕様を検証するための型システム 既存の型システムは仕様が有限状態オートマトンで記述できる場合についてのものであった。これを拡張してよりクラスであるプッシュダウンオートマトンで記述できる仕様などについても適用できるように型システムを拡張し,型付け可能性が決定可能のなるための十分条件を示した.また提案手法を用いて,既知の最も強い結果である文脈自由言語と超決定性言語の包含判定の決定可能性を証明し,提案手法の有効さを示した.この結果は従来よりも広い範囲の仕様(例えば出力のXML文書が与えられたDTDを満たすかどうか)に対する,高階関数型プログラムの自動検証に応用するとができる.2.型システムの逆像計算への応用高階再帰スキームのための型システムを応用することで,高階木トランスデューサーの逆像計算という問題が解けるということを示した.逆像計算とは出力から入力を求める計算のことで,様々な計算モデルについて研究されてきていた.逆像計算問題と(順方向の)計算の検証問題との関連は指摘されていたが,我々ははじめて厳密な対応関係を示した.
|
