高機能高品質ソフトウエアの基礎理論に関する研究

1992 Fiscal Year Annual Research Report

• Project/Area Number: 04219102
• Research Institution: Tohoku University
• Principal Investigator: 伊藤 貴康 東北大学, 工学部, 教授 (80124551)
• Co-Investigator(Kenkyū-buntansha): 榎本 肇 芝浦工業大学, 工学部, 教授 (60016227) ; 井田 哲雄 筑波大学, 電子情報工学系, 教授 (70100047) ; 林 晋 龍谷大学, 理工学部, 教授 (40156443) ; 萩谷 昌己 東京大学, 理学部, 助教授 (30156252) ; 佐藤 雅彦 東北大学, 電気通信研究所, 教授 (20027387)
• Keywords: 高機能高品質ソフトウエア / 構造化ネット / ATMSを用いた項書換え系 / 構成的プログラミング / 型理論とプログラム抽出 / 証明チェッカ / 項書き換系とナローイング / ソフトウエアプロセスの記述

Research Abstract

高機能高品質ソフトウエアとその構成原理についての基礎的な理論研究を行うと共に、理論に基づいてソフトウエアの構成・検証・記述を支援するシステムを試作し、実験的に評価した。
伊藤は、構造化ネットと並列プロセスのネット表現の研究を行い、構造化ネット操作システムを試作した。また、ATMSを用いた項書き換え系の実現方式とその試作・評価の研究を行った。
佐藤は、構成的プログラミングのための論理体系として、構成的数学体系RPTを作成し、これをRPTシステムとして計算機上で実現し、プログラムの検証・合成が行えることを示した。
萩谷は、高階の型理論に基づく証明チェッカを汎用テキストエディタ上に構築すると共に、図形を用いた証明の基礎付けを与えることにより、証明の中の図形を計算機上で形式的に扱う枠組みを提唱した。
林は、singleton,union,intersectionの型を持つ型理論としてATTとAGTTを提唱し、これらを用いるとプログラムの抽出がより明解に行え、かつ、効果のよいプログラムの抽出がでることを示した。
井田は、項書き換え系に基づく遅延ナローイング計算系の研究を行い、関数・論理融合型プログラミング言語に対する遅延ナローイング計算系の設計およびその完全性の証明、制約評価系の遅延ナローイング計算系への導入の研究を行った。
榎本は、ソフトウエアプロセス全体の流れの記述に関して、TELLシステムを設計・試作し、TELLシステムを用いて、カラー画像描画と処理の統合を目指したシステムの作成を行った。

Research Products

• [Publications] 川本 真一,伊藤 貴康: "並列プロセスのネット表現" 日本ソフトウエア科学会第9回論文集. (1992)
• [Publications] Masahiko Sato: "Adding proof objects and inducitve definition mechanism to frege structures" Springer LNCS. 526. 53-87 (1991)
• [Publications] 萩谷 昌己: "テキスト・エディタ上の証明チェッカ" 情報処理学会 プログラミング-基礎・実践・言語-研究会資料. PRG7-9. (1992)
• [Publications] Susumu Hayashi: "Siugleton,Union and Intersection Types for Program Extraction" Springer LNCS. 526. 710-730 (1991)
• [Publications] Y.Moriya,N.Niwa,Y.Murao,H.Enomoto: "Concurrent Schema of Cooperative picture painting system" Proc.Visual Communications and Image Processing. 1818. 1531-1544 (1992)
• [Publications] 井田 哲雄,松野 年宏: "MC/LISP処理系の翻訳系の構成" コンピュータ・ソフトウエア. 8. 53-67 (1992)