| 研究概要 |
本研究は関数型プログラミング言語向けの検証支援システムの開発を目標にしている.そのシステムの主要ルーチンである(整数上の変数込みの大小判定を含む)プレスブルガー文真偽判定ルーチンを関数型プログラミング言語MLを用いて作成し,その有用性の評価を行なった.その評価の一部として,京都大学作成の教育用CPU KUE-CHIP2の設計検証の一部(命令のプリフェッチの導入による詳細化)に適用し,実用規模の例題に対しても1秒以下で検証可能なことを示した.また,検証支援システムについては学生と共同で関数型プログラミング言語OCAMLを用いて,鋭意作成中である.上述のプレスブルガー文真偽判定ルーチンの有用性,検証支援システムの設計方針,詳細設計について2004年3月に行われる電子情報通信学会のソフトウェアサイエンス研究会で発表する.
検証支援システムのプロトタイプは4月中にできる予定である.
適用例題については従来の研究グループのノウハウを活用しつつ,図書管理システムで行う予定である.このシステムのモジュール設計,仕様記述の一部をすでに行っている.モジュールは大きく3つに分かれる.
個々のモジュールに対して,要求すべき性質記述を,ソースプログラムのコメント記述部に定められたフォーマットに沿って記述するスタイルを採る.提案する検証方法では,記述された要求記述とプログラム本体の記述から型付きTRSによる等価変換を経て,プレスブルガー文に変形する.
今後は開発を完了し,例題適用を行って,開発効率,問題点などについて調べ,本研究で得られる知見についてまとめる.
|
