Smart Programming Environments

对于快速开发可靠的软件来说，类型安全是高级编程环境必不可少的特征，但仅有类型安全是不够的。程序员试图通过对程序行为的推理来消除尽可能多的错误。为了支持这一活动，本研究寻求设计和构建智能编程环境。智能编程环境是用于编写、编辑、执行和分析程序的系统。对于后者，环境包括“软类型检查器”，用于验证简单程序不变量的工具。最值得注意的是，这些是每个程序操作的前提条件。基于不同的分析方法，开发了两种方案软类型检查器原型。一种是对Hindley-Milner类型推理的改进（对于非标准类型代数）；另一种使用基于集合的分析形式。本研究将扩展这些工具，并寻求(1)开发一类新的软类型，结合Hindley-Milner和基于集的分析的优势，(2)合并额外的验证技术，(3)开发用于探索验证者推理的替代接口，以及(4)扩展模块化编程工具。此外，正在探索将该技术转移到较低级语言的方法，例如编程环境中的c++的安全子语言（类似于Java）。＊＊＊

Type safety is an essential feature of advanced programming environments for the rapid development of reliable software, but it is not sufficient. Programmers try to eliminate as many errors as possible by reasoning about the program's behavior. To support this activity, this research seeks to design and construct smart programming environments. A smart programming environment is a system for writing, editing, executing, and analyzing programs. For the latter, the environment includes "soft type checkers", tools for verifying simple program invariants. Most notably, these are the preconditions for each program operation. Two prototypes of soft type checkers for Scheme have been developed, based on different analysis methods. One uses an adaptation of Hindley-Milner type inference (for a non- standard type algebra); the other uses a form of set-based analysis. This research would extend the tools, and seeks (1) to develop a new class of soft typers that combine the advantages of Hindley-Milner and set-based analysis, (2) to incorporate additional verification technology, (3) to develop alternative interfaces for exploring the verifier's reasoning, and (4) to extend the tools for modular programming. In addition, ways are being explored to transfer the technology to lower-level languages, such as a safe sublanguage of C++ (similar to Java) in the programming environment. ***