| 研究課題/領域番号 |
04219102
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
伊藤 貴康 東北大学, 工学部, 教授 (80124551)
|
|---|
| 研究分担者 |
榎本 肇 芝浦工業大学, 工学部, 教授 (60016227)
井田 哲雄 筑波大学, 電子情報工学系, 教授 (70100047)
林 晋 龍谷大学, 理工学部, 教授 (40156443)
萩谷 昌己 東京大学, 理学部, 助教授 (30156252)
佐藤 雅彦 東北大学, 電気通信研究所, 教授 (20027387)
|
|---|
| キーワード | 高機能高品質ソフトウエア / 構造化ネット / ATMSを用いた項書換え系 / 構成的プログラミング / 型理論とプログラム抽出 / 証明チェッカ / 項書き換系とナローイング / ソフトウエアプロセスの記述 |
|---|
| 研究概要 |
高機能高品質ソフトウエアとその構成原理についての基礎的な理論研究を行うと共に、理論に基づいてソフトウエアの構成・検証・記述を支援するシステムを試作し、実験的に評価した。
伊藤は、構造化ネットと並列プロセスのネット表現の研究を行い、構造化ネット操作システムを試作した。また、ATMSを用いた項書き換え系の実現方式とその試作・評価の研究を行った。
佐藤は、構成的プログラミングのための論理体系として、構成的数学体系RPTを作成し、これをRPTシステムとして計算機上で実現し、プログラムの検証・合成が行えることを示した。
萩谷は、高階の型理論に基づく証明チェッカを汎用テキストエディタ上に構築すると共に、図形を用いた証明の基礎付けを与えることにより、証明の中の図形を計算機上で形式的に扱う枠組みを提唱した。
林は、singleton,union,intersectionの型を持つ型理論としてATTとAGTTを提唱し、これらを用いるとプログラムの抽出がより明解に行え、かつ、効果のよいプログラムの抽出がでることを示した。
井田は、項書き換え系に基づく遅延ナローイング計算系の研究を行い、関数・論理融合型プログラミング言語に対する遅延ナローイング計算系の設計およびその完全性の証明、制約評価系の遅延ナローイング計算系への導入の研究を行った。
榎本は、ソフトウエアプロセス全体の流れの記述に関して、TELLシステムを設計・試作し、TELLシステムを用いて、カラー画像描画と処理の統合を目指したシステムの作成を行った。
|
