構成的プログラミングを実現する証明、検証、合成システム

1994 Fiscal Year Annual Research Report

• Project/Area Number: 06452387
• Research Institution: Tohoku University
• Principal Investigator: 佐藤 雅彦 東北大学, 電気通信研究所, 教授 (20027387)
• Co-Investigator(Kenkyū-buntansha): 亀山 幸義 東北大学, 電気通信研究所, 助手 (10195000) ; 龍田 真 東北大学, 電気通信研究所, 助教授 (80216994)
• Keywords: 構成的プログラミング / 構成的論理 / 直観主義論理 / プログラム検証 / プログラム合成

Research Abstract

本研究の大目的は、ソフトウェアの生産が手作業で行なわれるため社会的に必要なソフトウェアの品質と量を確保することができないといういわゆるソフトウェアの危機を解決するために、誤りのないプログラムを自動的に生産するシステムを実現するための基礎理論を構築することである。本研究代表者が提唱した構成的プログラミングの方法に基づくプログラム合成システムは、この問題の有力な解決策である。
本研究の目的は、構成的プログラミングの基礎理論に関する理論的研究を深化させるとともに、構成的プログラミングを実現するための証明、検証、合成システムの試作システムを作成することである。
本研究では、本研究全期間内において、構成的プログラミングの基礎理論の構築のため、プログラミング言語Λの設計を完成させ、また、理論体系RPTの研究を深め、これを完成する。また、プログラミング言語Λの処理系および理論体系RPTの証明システムを計算機上に実現する。PRTの証明システムを用いて、Λのプログラムの検証、合成システムを計算機上に実現する。
今年度の研究では、論理体系RPTおよびプログラム言語Λの基本設計について理論的考察を加えた。特に、Λにどのようにして広域代入の概念をもつよう拡張するかについて考察した。また、プログラム言語Λの解釈系、翻訳系を、本研究経費で購入するワークステーション上に実現した。PRTの証明、検証システムをプログラム言語Λにより実現するためのプログラミング環境を整備した。

Research Products

• [Publications] 亀山幸義: "自己反映的証明体系RPTの理論と実現" コンピュータソフトウェア. (出版予定).
• [Publications] Y.Kameyama: "A type-free theory of half-positive inductive defivitions and its application" International Journal of Foundations of Computor Science. (出版予定).
• [Publications] M.Tatsuta: "Two realizability interpretations of monotone inductive definitions" International Journal of Foundations of Computor Science. 5. 1-21 (1994)