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

点击翻译按钮获取中文摘要

本研究は関数型プログラミング言語向けの検証支援システムの開発を目標にしている.昨年度までにそのシステムの主要ルーチンである(整数上の変数込みの大小判定を含む)プレスブルガー文真偽判定ルーチンを関数型プログラミング言語MLを用いて作成し,その有用性の評価を行なった.今年度は検証手法を確定し,検証支援システムを試作した.まず,モジュールごとに記述された「契約に基づく設計」に沿ったモジュール仕様を等式集合として表し,それらのモジュール仕様の各等式を管理しやすいようにXMLタグを用いて管理する方法を考案した.次いで,この仕様とプログラム本体から検証式を自動作成し,正しさの検証をプレスブルガー文真偽判定に帰着させる判定手法を考案し,その検証手法を6月に岡山で行われたソフトウェアシンポジウム2004(査読あり)にて発表した.次いで,この検証手法に基づき,関数型言語ML向けにOCaMLを用いて作成した検証支援システムを9月に函館で行われたソフトウェアサイエンス研究会にて発表した.検証例題として図書管理システムを選び,プログラム作成と仕様作成を行った.このシステムは大きく6つのモジュールで構成される.この中で主要なモジュールである貸し出しモジュールに対し,下位のデータベース操作モジュールの仕様の正しさを仮定した上で,正しく貸し出しが行われること(そのようにプログラムが実装されていること)の検証作業をこの検証支援システムを実際に用いて行った.その結果,検証作業に不慣れな学生であっても,従来手法と遜色のない手間と時間でできることがわかった.この結果は,3月に行われたPPL2005(プログラムおよびプログラム言語ワークショップ2005)で発表し,デモ公開した.