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

高性能、高质量软件基础理论研究

• 批准号: 04219102
• 负责人: 伊藤 貴康
• 金额: $ 10.11万
• 依托单位: Tohoku University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research on Priority Areas
• 财政年份: 1992
• 资助国家: 日本
• 起止时间: 1992 至 无数据
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-04219102/
• 关键词: 高機能高品質ソフトウエア; 構造化ネット; ATMSを用いた項書換え系; 構成的プログラミング; 型理論とプログラム抽出; 証明チェッカ; 項書き換系とナローイング; ソフトウエアプロセスの記述

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

The theoretical study of the principle of high-quality equipment and high-quality equipment. The theoretical study of the basic theory of high-quality equipment, high-quality, high-quality, high-quality, Ito, the construction of the system, and the list of information about the performance of the research and the operation of the system. This is done in the way that the project is implemented, and the ATMS is used as a research tool. Sato, the mathematical system constructed by Sato, the mathematical system constructed by The basic theory of high-level and high-level theory is that the information system is used to display the information on the computer system, the system, the computer, the computer and the computer. Lin Yun, singleton,union, intersectionist theory, holding theory, "ATT", "AGTT", "raise", "draw", "please", "please" and "please". Ikeda and project systems are based on the system of computer science, the system, the computer, the computer, the computer. In this paper, the whole system is used to record the data flow of the whole system, such as the design of the device, the design of the device, the portrait of the device and the system.

项目成果

川本 真一,伊藤 貴康: "並列プロセスのネット表現" 日本ソフトウエア科学会第9回論文集. (1992)

Shinichi Kawamoto、Takayasu Ito：“并行过程的网络表示”日本软件科学会第 9 届会议论文集（1992 年）。

Susumu Hayashi: "Siugleton,Union and Intersection Types for Program Extraction" Springer LNCS. 526. 710-730 (1991)

Susumu Hayashi：“用于程序提取的 Siugleton、并集和交集类型”Springer LNCS。

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)

Y.Moriya，N.Niwa，Y.Murao，H.Enomoto：“协作绘画系统的并发模式”Proc.视觉通信和图像处理。

井田 哲雄,松野 年宏: "MC/LISP処理系の翻訳系の構成" コンピュータ・ソフトウエア. 8. 53-67 (1992)

Tetsuo Ida，Toshihiro Matsuno：“MC/LISP 处理系统的翻译系统配置”计算机软件。8. 53-67 (1992)。

Masahiko Sato: "Adding proof objects and inducitve definition mechanism to frege structures" Springer LNCS. 526. 53-87 (1991)

Masahiko Sato：“向弗雷格结构添加证明对象和归纳定义机制”Springer LNCS。