Smart Programming Environments

点击翻译按钮获取中文摘要

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. ***