関数型プログラムに対するモジュール構造を考慮にいれた効率のよい形式的検証支援

2002 Fiscal Year Annual Research Report

• Project/Area Number: 14780214
• Research Institution: Osaka University
• Principal Investigator: 岡野 浩三 大阪大学, 大学院・情報科学研究科, 助教授 (70252632)
• Keywords: 関数型プログラム言語 / 定理証明 / プレスブルガー文 / 項書換え系 / ML

Research Abstract

ML等の関数型プログラムを念頭にプログラムの正しさを保証できる開発支援システムの構築を行うことにより,形式的証明支援システムや関数型プログラム言語の実用性の限界を調べることを目的としている.
特にMLにおいてはシグネチャ機構により,外部公開される関数,変数と,情報隠蔽される情報との区別が行われる.そのシグネチャ記述に加え,モジュールの満たすべき性質を代数的記述に準じた形式記述で行い,正しさの保証を伴ったプログラム開発を行えることを目指す.
本年度はこの開発支援支援システムのうち証明支援システムの主要部となる「プレスブルガー文真偽判定処理系」と「多ソート対応項書き換えシステム(多ソートTRS)」をMLで実装した.これまでの研究においては限定されたクラスに対する高速プレスブルガー文真偽判定処理系や多ソートTRSをC言語で実装しているのに対して,今回は完全なクラスのプレスブルガー文真偽判定処理系とKnuth-Bendix完備化アルゴリズムを内蔵する多ソートTRSをMLで記述,実装している.従来の研究の成果を取り入れ,限定されたプレスブルガー文に対しては高速に判定しながらも通常のプレスブルガー文にも対応できるよう工夫している.
このプレスブルガー文真偽判定処理系については世界に公開されている米国メリーランド大学のΩ処理系と比較を行い,判定時間に遜色のないことを確認した.この結果,MLによるプログラム記述および実装を通してC言語による実装に比べて開発期間,実行速度ともに遜色ないという結論を得た.また関数型プログラム開発上の問題点をいくつか確認した.さらに実行効率の評価をした上で研究会に発表すべく鋭意準備中である.