Constructive Programming System for Proof Development, Verification, and Program Synthesis

用于证明开发、验证和程序综合的构造性编程系统

• 批准号: 06452387
• 负责人: SATO Masahiko
• 金额: $ 4.61万
• 依托单位: KYOTO UNIVERSITY (1995)Tohoku University (1994)
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for General Scientific Research (B)
• 财政年份: 1994
• 资助国家: 日本
• 起止时间: 1994 至 1995
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-06452387/
• 关键词: Constructive Programming; Constructive Logic; Proof Development System; Functional Programming; Assignment Statement; Lazy evaluation; 関数型プロゲーム言語; 直観主義論理; プログラム検証; プログラム合成

In this research project, we designed and improved the constructive logical system RPT and analyzed its properties. We also implemented a proof-development system based on RTP.By using this system, we can demonstrate the paradigm of Constructive Programming.RPT was designed to be a basic logical system for constructive programming ; a unique feature of RPT is that it has a reflective tower ; we can internally express meta-expressions in RPT.The terms of RPT correspond to programs of a certain functional programming language, which we call A.We first gave a formal system of RPT,and then proved several proof-theoretic properties of RPT such as consistency. We then implemented an interpreter and a compiler of A on top of UNIX workstations. We pointed out the problem of inefficiency when we adopt lazy-evaluation strategy for programming languages with assignment statements. We proposed a program transformation technique which fixes this problem.We finally implemented by A a proof-development system which provides supports for developmoent of proofs of RPT.By using this system, we can prove properties of A programs. As a substantial example, we presented a mechanized proof of Church-Rosser theorem. We also presented a concrete example of Constructive Programming ; namely, we developed a proof of a specification formula of a certain program, and the extracted a verified program from the proof.

在本课题中，我们设计并改进了构造逻辑系统RPT，并对其性质进行了分析。我们还实现了一个基于RTP的验证开发系统。通过使用这个系统，我们可以展示建设性规划的范例。RPT被设计成构造性编程的基本逻辑系统；RPT的一个独特之处在于它有一个反射塔；我们可以在RPT中内部表达元表达式。RPT的项对应于某种函数式编程语言的程序，我们称之为a。我们首先给出了RPT的一个形式化系统，然后证明了RPT的几个证明理论性质，如一致性。然后我们在UNIX工作站上实现了a的解释器和编译器。我们指出了对带有赋值语句的编程语言采用延迟求值策略时效率低下的问题。我们提出了一种程序转换技术来解决这个问题。我们最终通过A实现了一个证明开发系统，为RPT的证明开发提供了支持。利用这个系统，我们可以证明A程序的性质。作为一个实质性的例子，我们给出了Church-Rosser定理的一个机械化证明。我们还提出了一个建设性规划的具体例子；即对某个程序的规范公式进行证明，并从证明中提取出一个已验证的程序。

项目成果

Masahiko Sato and Yukiyoshi Kameyama: "Conservativeness of A over lambdasigma-calculus" Lecture Notes in Computer Science. 792. 73-94 (1994)

Masahiko Sato 和 Yukiyoshi Kameyama：“A 在 lambdasigma 演算上的保守性”计算机科学讲义。

Satoshi Kobayashi: "Realizability Interpretation of Generalized Inductive Definitions" Theoretical Computer Science. 131-1. 121-138 (1994)

Satoshi Kobayashi：“广义归纳定义的可实现性解释”理论计算机科学。

Masahiko Sato: "A Nootural Deduction System with Catch/Throw Rules" The Secerd Worksop on Starlard Logic and Cogical Aspects of Computpr Science. (1995)

Masahiko Sato：“带有捕获/抛出规则的 Nootural Deduction System” 关于 Starlard 逻辑和计算机科学的 Cogical Aspects 的 Secerd Worksop。

Masahiko Sato: "A Purely Functional Language with Encapsulated Assignment" Lecture Notes in Computer Science. 789. 179-202 (1994)

Masahiko Sato：“带有封装作业的纯函数式语言”计算机科学讲义。

Yukiyoshi Kameyama: "A type-Free Theony of Half-Morotone Inductive Definitions" International Journal of Foundations of Computer Science. 6-3. 203-234 (1995)

Yukiyoshi Kameyama：“半莫罗通归纳定义的无类型理论”国际计算机科学基础杂志。