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

2003 年度 実績報告書

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

研究課題

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

研究代表者

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

キーワード関数型プログラミング言語ML / 型付TRS / プレスブルガー文 / 図書管理システム / 検証支援システム
研究概要

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

  • 研究成果

    (1件)

すべて その他

すべて 文献書誌 (1件)

  • [文献書誌] 才村 徹也: "関数型言語MLによるプレスブルガー文真偽判定ルーチンの開発"電子情報通信学会技術報告. SS2003-47. 7-12 (2004)

URL: 

公開日: 2005-04-18   更新日: 2016-04-21  

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

Powered by NII kakenhi