代数的仕様記述法に基づくソフトウェア開発支援

1988 年度 研究成果報告書概要

• 研究課題/領域番号: 62880007
• 研究種目: 試験研究
• 配分区分: 補助金
• 研究分野: 情報学
• 研究機関: 名古屋大学
• 研究代表者: 稲垣 康善 名古屋大学, 工学部, 教授 (10023079)
• 研究分担者: 椎野 努 沖電気工業, 研究開発本部総合システム研究所, 部長 ; 太田 義勝 名古屋大学, 大型計算機センター, 助手 ; 平田 富夫 名古屋大学, 工学部, 助教授 (10144205) ; 坂部 俊樹 名古屋大学, 工学部, 助教授 (60111829) ; 吉田 雄二 名古屋大学, 工学部, 教授 (50023247) ; OHTA Yoshikatsu Computation Center, Nagoya University ; SHIINO Tsutomu Research & Development Group, Oki Electric Industry Co., Ltd.
• 研究期間 (年度): 1987 – 1988
• キーワード: ソフトウェア / 代数的仕様記述 / データ型 / 型構成子 / 直接実現 / 項書換え系 / プロトタイピング / 段階的詳細化

研究概要

本研究の目的は、代数的手法によるソフトウェアの仕様記述、検証、自動合成を支援するシステムの実用化のための基礎的技法を明らかにすることである。このため、1.使い易い代数的仕様記述言語の開発、2.代数的仕様の直接実現系の高速化、3.代数的仕様記述向きの高機能エディタの設計と実現、4.仕様とプログラムの再利用のための知的データベースシステムの作成、を具体的な目標として研究をすすめた。その結果、以下にのべる成果を得ることができた。
まず、1.に対しては、代数的仕様記述と手続き的記述とを混在させてプログラムを書くという新しいプログラミングスタイルを許すため、代数的仕様の階層的記述機能を持つ手続き型言語Ultra Cを設計し、その処理系を開発した。この処理系では、階層的に記述した代数的仕様モジュールの分割コンパイルが可能であり、階層的な記述機能とともに、ソフトウェア開発過程の効率化に役立つ。
2.については、代数的仕様の直接実現系Cdimpleを開発した。Cdimpleは代数的仕様をC言語のプログラムに変換するシステムである。得られたCプログラムはプロトタイピング用としては十分な実行速度を持つ。また、仕様が変更されても、改めてCdimpleを再起動せずにすむように改良も加えた。
3.については、代数的仕様記述のためのフロント・エンドの設計を行い、その実現を行っている。
4.については、代数的仕様の検索機能の実現に欠かせない仕様の性質の検証ツールを開発した。
以上のように、代数的手法に基づく種々のソフトウェア開発支援ツールを開発し、代数的手法の実用化のための問題点をさぐり、その解決の目度を立てることができた。これによって、代数的手法に基づくソフトウェア開発環境の構築への見通しを得ることができ、更に今後の研究開発実用化への将来展望を得ることができた。

研究成果

• [文献書誌] 北英彦: 人工知能学会誌. 2. 375-378 (1987)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] 酒井正彦: コンピュータソフトウェア. 4. 16-27 (1987)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] 北英彦: 電子情報通信学会論文誌. J70-D. 2428-2437 (1987)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] 直井徹: 電子情報通信学会論文誌. J71-D. 942-949 (1988)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] 直井徹: 電子情報通信学会論文誌. J71-D. 1893-1900 (1988)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] 平田富夫: 情報思慮学会アルゴリズム研究会. 88-AL-4. 4・1・1-4・1・7 (1988)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] 酒井正彦: 電子情報通信学会技術研究報告. COMP88-95. 37-40 (1989)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] 酒井正彦: 電子情報通信学会技術研究報告. COMP88-86. 83-92 (1989)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] 山本晋一郎: 電子情報通信学会技術研究報告. COMP88-94. 41-50 (1989)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] 山中英樹: 電子情報通信学会技術研究報告. COMP88-96. 61-70 (1989)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] 山本隆弘: 昭和63年度情報処理学会全国大会論文集. 1130-1131 (1989)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] 北英彦: 電子情報通信学会論文誌. (1989)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] Hidehiko, Kita: "Algebraic Approach to Program Verification" Journal of Japanese Society for Artificial Intelligence. 2. 375-378 (1987)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] Masahiko, Sakai: "Direct Implementation System of Algebraic Specifications of Abstract Daty Types" Computer Software. 4. 16-27 (1987)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] Hidehiko, Kita: "An Algebraic Specification of a Pascal-like Programming Language PL/O+" The Transaction of IEICE. J70-D. 2428-2437 (1987)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] Tohru, Naoi: "Semantics of Term Rewriting Systems and Free Continuous Algebra" The Transaction of IEICE. J71-D. 942-949 (1988)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] Tohru, Naoi: "The Relation between Algebraic and Behavioroul Semantics of Term Rewriting Systems and Their Conservative Extensions" The Transaction of IEICE. J71-D. 1893-1900 (1988)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] Tomio, Hirata: "Tree Pattern Matching Algorithms" Society of Japan of Information Processing Technical Report. 88-AL-4. 1-7 (1988)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] Masahiko, Sakai: "A Method for Proving Inductive Properties of Algebraic Specifications" IEICE Technical Report. COMP88-86. 83-92 (1989)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] Masahiko, Sakai: "An Implementation of TRS Interpreter with Compliling Facility" IEICE Technical Report. COMP88-93. 37-40 (1989)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] Shinichiro, Yamamoto: "An Inplementation of Parallel-Outermost Strategy for TRS Interpreter" IEICE Technical Report. COMP88-94. 41-50 (1989)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] Hideki, Yamanaka: "Compilation of Regular Term Rewriting Systems into Constructor Ones with Call-by-Value Strategy" IEICE Technical Report. COMP88-96. 61-70 (1989)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] Takahiro, Yamamoto: "Ultra C with Hierarchical Algebraic Specification" Proc. of IPSS Spring National Conference. 1130-1131 (1989)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] Hidehiko, Kita: "Soundness of an Axiom System for Algebraic Semantics of a Programming Language" The Tranzation of IEICE. To Appear. (1989)
  • 説明: 「研究成果報告書概要(欧文)」より