2012 Fiscal Year Annual Research Report
モジュラー書換え理論に基づく代数型ソフトウェア開発言語の構築
| Project/Area Number |
22700027
|
|---|
| Research Institution | Toyama Prefectural University |
|---|
Principal Investigator |
中村 正樹 富山県立大学, 工学部, 講師 (40345658)
|
|---|
| Project Period (FY) |
2010-04-01 – 2013-03-31
|
| Keywords | 代数仕様 / 項書換えシステム / モジュールシステム / テスト生成 / プログラム変換 / 形式手法 |
|---|
| Research Abstract |
本研究では，ソフトウェア開発における形式手法・形式的検証の大衆化を目指し，ソフトウェア開発工程の全体を一貫して取り扱うことが可能な言語を構築し，研究者ではない一般ソフトウェア開発者にも利用可能な支援環境を提供することを目的とする．厳密な数学的モデルを持ち形式的検証も可能な代数仕様を中心に，仕様の作成・検証からプログラムコードの実装・テストまでに現れる代数仕様とプログラムコードが入り交じった"半仕様・半実装"の取り扱いが可能な代数型ソフトウェア開発言語の構築を目指す．最終年度では，本研究課題における最終成果物となる代数型ソフトウェア開発言語の実装，および，同言語における仕様作成支援ツールの基礎的研究を行った．前者では，前年度の研究成果である"Translation of State Machines from Equational Theories into Rewrite Theories with Tool Support" (2011, Min Zhang, et al.) に基づき，Maude言語上での本開発言語の実装を試みた．後者では，本開発言語で取り扱う仕様（半仕様・半実装）実行の際に重要となる項書き換えシステムの基本的性質（主に停止性）の判定ツール実装に向け，その前段階として，現行の代数仕様言語（OBJ族）に対して，モジュール構造に基づく軽量な判定手法を提案し，"A Hierarchical Approach to Operational Termination of Algebraic Specifications" および "Incremental Proofs of Operational Termination with Modular Conditional Dependency Pairs"として国際会議にて発表した．
|
| Current Status of Research Progress |
Reason
24年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
24年度が最終年度であるため、記入しない。
|
