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