Smart Programming Environments

智能编程环境

• 批准号: 9633746
• 负责人: Robert Cartwright
• 金额: --
• 依托单位: William Marsh Rice University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1996
• 资助国家: 美国
• 起止时间: 1996-09-01 至 1999-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9633746&HistoricalAwards=false
• 关键词: 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. ***

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