• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2002 年度 実績報告書

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

研究課題

研究課題/領域番号 14780214
研究機関大阪大学

研究代表者

岡野 浩三  大阪大学, 大学院・情報科学研究科, 助教授 (70252632)

キーワード関数型プログラム言語 / 定理証明 / プレスブルガー文 / 項書換え系 / ML
研究概要

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

URL: 

公開日: 2004-04-07   更新日: 2016-04-21  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi