非停止プロセスの抽象化と代数的仕様記述に関する基礎的研究

1989 Fiscal Year Annual Research Report

• Project/Area Number: 63580025
• Research Institution: Nagoya University
• Principal Investigator: 坂部 俊樹 名古屋大学, 工学部, 助教授 (60111829)
• Co-Investigator(Kenkyū-buntansha): 平田 富夫 名古屋大学, 工学部, 助教授 (10144205) ; 稲垣 康善 名古屋大学, 工学部, 教授 (10023079)
• Keywords: 非停止プロセス / 等式論理 / 代数的仕様記述 / 並行プロセス / CCS / 木パタ-ンマッチング

Research Abstract

本年度の研究実績は以下の通りである。
1.非停止プロセスが陽に記述できる有理等式論理の拡張については、論理の意味の研究が進められた。すなわち有理等式論理の基本構文である項書換え系の代数的意味論と計算複雑さについての研究に基づく項書換え系の等価交換法を示し、その正当性を証明した。
2.代数的仕様記述言語の設計及び処理系の開発については、最外戦略による項書換えアルゴリズムについて研究し、代数的言語の処理系の開発の基礎を確立した。
3.仕様の検証法についての検討では、仕様の帰納的定理の証明法について研究した。この研究では、従来の構造帰納法を拡張した被覆集合に基づく構造帰納法を提案し、その証明法による証明支援システムの開発に着手した。
4.CCSと有理等式論理の関係の解明については、両者の意味論の対応をとるため、CCSの意味論を中心に研究を行った。すなわち、CCSの意味論として観測等価関係を採用し、それによって並行処理の基本モデルであるモニタの排他制御、同期制御、抽象化機構が自然に説明できることを明らかにした。
5.その他、研究計画に挙げられていない項目として、関数型の並行プロセスのモデルとして通信機能付項書換え系を考案した。主な結果はプロセス内計算とプロセス間通信計算の独立性と計算の一意味を示したことである。

Research Products

• [Publications] 北英彦: "プログラミング言語の代数的意味論に対する公理的検証体系の健全性" 電子情報通信学会論文誌. J72-D-I. 377-386 (1989)
• [Publications] Tohru Naoi: "Algebraic Semanstics and Complexity of Term Rewriting Systems" Proc.of ACM 3rd International Conference on Rewriting Techniqre and Applications. 311-325 (1989)
• [Publications] 坂部俊樹: "代数的仕様作成支援のための基本ツ-ル" 平成元年度電気関係学会東海支部連合大会予稿集. S-84-S-87 (1989)
• [Publications] 松繁孝紀: "通信機能付き項書換え系" 平成元年度ソフトウエア科学会全国大会論文集. 209-212 (1989)
• [Publications] 田中義憲: "代数的意味論に基づく項書換え系の等価変換手続き" 平成元年度ソフトウエア科学会全国大会論文集. 213-216 (1989)
• [Publications] 結縁祥治: "CCSの意味論とその拡張" 平成元年度電気・情報関連学会連合大会予稿集. 5-63-5-66 (1989)