Design of Proving, Verifying, and Synthesizing System based on Constructive

本项目对建设性规划的核心思想进行了非常深入的研究。构造性程序设计是程序设计方法论中的一种新范式，它以构造性逻辑系统为基础理论，为程序的验证、数学定理的证明和程序的逻辑规范综合提供了严格统一的基础。我们的主要研究结果总结如下：1。我们设计了一个组织良好的建设性逻辑系统。从某种意义上说，海温是象征性的，因为所有的项和公式都可以机械地处理，因此可以用计算机处理。SST是编写规范（作为集合的数据类型）和对程序属性进行推理的合适逻辑，因为SST是部分项的一阶谓词逻辑。我们建立了理论结果。我们首先做了一个海温模型来证明海温是一致的。这个模型反映了我们期望的s表达式域。我们证明了一般递归函数的表示定理。然后定义了海表温度的形式化可实现性解释。这种解释类似于所谓的q-可实现性，但我们将其改进为允许任意归纳定义。我们证明了我们可实现性解释的合理性。SST包含一个纯函数式编程语言LAMBDA。LAMBDA由海表温度中的封闭项组成。它是纯函数式的，但为了实用方便，我们将其扩展为LAMBDA+。我们在一个工作站上实现了LAMBDA解释器。我们在LAMBDA上编写了几个系统。我们制作了LAMBDA本身的元循环解释器、SST的证明检查系统和程序提取器LAMBDA。我们可以通过证明检查系统本身来推断这些程序的性质。程序提取器从SST.5的证明中提取lambda程序。使用上述系统，我们通过实例检验了建设性规划的概念。我们进行了样本证明，并通过证明检查系统检查其有效性，并通过程序提取器提取计算部分。作为这个过程的反馈，我们改进了SST和LAMBDA，使这些系统变得更加简单和易于处理。少

This project has investigated the key-idea constructive programming very thoroughly. Constructive programming is a new paradigm in programming methodology, which takes constructive logical system as an underlying theory and provides a rigid and uniform basis for verifying programs, proving mathematical theorems, and synthesizing programs from its logical specifications.Our main results are summarized as follows:1. We designed a well-organized constructive logical system SST. SST is symbolic in the sense that all terms and formulas can be treated mechanically, and therefore, by computers.SST is a suitable logic for writing specifications (datatypes as sets), and for reasoning about properties of programs, since SST is a first order predicate logic for partial terms.2. We established the theoretical results. We first made a model of SST to show SST is consistent. This model reflects our intended domain of S-expressions. We proved the representation theorem for general recursive functions … More in SST. We then defined the formalized realizability interpretation of SST. This interpretation resembles so called q-realizabilty, but we refined it to allow arbitrary inductive definition. We proved the soundness of our realizability interpretation.3. SST contains a pure functional programming language LAMBDA. LAMBDA is formed by taking closed terms in SST. It is purely functional, but for practical conveniences, we extended it to LAMBDA+. We implemented the interpreter of LAMBDA on a workstation.4. We programmed several systems on top of LAMBDA. We made a metaeircular interpreter of LAMBDA itself, a proof-checking system of SST, and a program-extractor LAMBDA. We can reason about the properties of these programs by the proof-checking system itself. The program-extractor extracts a LAMBDA-program from a proof in SST.5. Using the above systems, we examined by examples the idea of constructive programming. We made sample proofs, and checked its validity by the proof-checking system, and extracted computational parts by the program-extractor.As a feed-back of this process, we refined SST and LAMBDA so that these systems become more simple and easy to treat. Less