Modular Program Analyses for Higher-Order Programming Languages

9619756该项目的基本目标是开发一个自动定理证明器，该证明器可以用高级数学编程语言对程序的性质进行推理。定理证明器将向程序员提供其分析结果，方法是在程序文本中添加注释的超链接和绘制图表。注释将描述一组值；图表将解释这些值的预期流。两者都可以用来在程序运行前了解程序的行为。因此，程序员将能够创建要么根本不会失败，要么只在一小部分定义良好的程序点上失败的程序。虽然这样的定理证明器的许多基本性质是理解的，但它们是否可以应用于包含数百或数千个相互依赖的模块的程序仍是一个悬而未决的问题。因此，该项目的中心目标是设计一个模块化的、可扩展的证明系统，证明它的正确性，设计一个合适的编程环境，并将定理证明器应用于它本身和它的编程环境。***

9619756 The basic goal of the project is to develop an automatic theorem prover that can reason about properties of programs in high- level, mathematical programming languages. The theorem prover will supply the results of its analysis to programmers by adding hyperlinks to annotations and drawing diagrams to the program text. The annotations will describe sets of values; the diagrams will explain the anticipated flow of these values. Both can be used to understand the program's behavior before it runs. As a result, programmers will be able to create programs that either do not fail at all or only fail at a small, well-defined set of program points. While many of the basic properties of such theorem provers are understood, it is an open question whether they can be applied to programs of hundreds or thousands of modules with mutual dependencies. Hence, the central goal of the project is to design a modular, scalable proof system, to prove its correctness, to engineer a suitable programming environment, and to apply the theorem prover to itself and its programming environment. ***