| 研究概要 |
平成18年度は,当初の計画に基づき,モジュラーな項書き換えシステム(MTRS)の理論に基づいて形式仕様言語CafeOBJ上に実装した仕様検証システムのプロトタイプを用い,仕様の記述,実験を行った.実験を通して得られて知見は以下の通りである.プロトタイプの摘用範囲と実際に作成される仕様の差異を明らかにし,実用的な適用範囲を持つようにMTRSの理論を拡張する必要があることがわかった.特にMTRSに基づく局所等価述語の実装に対して明らかにする必要がある.ただし適用範囲は,周辺分野の研究の進歩にしたがい日々変わっていくものであるため,本研究で提案する推論エンジンでは,適用条件の判定機能をモジュール化し,当面はすでにわかっている簡単な条件を採用することとした.採用する条件であっても十分に実用的であり,既存の多くの仕様に適用可能であることがわかっている.証明スコアの調査分析では,所属する研究室のメンバらとの打ち合わせを通し,既存の仕様例をもとに,システムマティックな証明スコアの作成手法がまとまりつつある。これらの成果は,既存のCafeOBJ検証システムに対するものがあるが,本研究課題で提案する検証システムにおいてもほとんどそのままの形で適用可能である.
関連する研究発表を以下に示す.上記の局所等価述語の適用条件のひとつである項書き換えシステムの停止性に関する研究成果が得られた(研究発表欄:Elimination Transformations for Associative-Commutative Rewriting Systems参照).振舞仕様の自動検証技術に関する研究成果は,本提案の検証システムにも将来的に役立つ技術である(同:Automating Invariant Verification of Behavioral Specifications参照).本研究課題の核となる理論が雑誌論文として採録された(同:モジュラーな代数仕様言語のための項書き換えシステム参照).また本提案の検証システムのプロトタイプを実際に用いた研究成果も得られた(同:A Behavioral Specification of mperative Programming Languages参照).
|
