A Smart Programming Environment for Java

9708957这个项目将着重于为Java构建一个“智能”编程环境，它使用语义分析来静态调试、验证和安全优化程序。主要研究人员已经为Scheme方言开发了这样一个环境的早期版本。安全的实现可以通过编译时分析、运行时检查和自动存储管理的组合来防止对基本程序操作的误用，比如取空列表的头。然而，安全性并不是万灵药：所有安全语言都将一些前提条件的检查推迟到运行时。当运行时检查失败时，程序执行将中止。因此，程序员试图通过分析每个基本操作的输入数据的形式来确保不可能出现错误应用。不幸的是，程序员并不擅长这项任务，而且经常犯错误。所建议的智能编程环境的主要目标是证明安全所需的运行时检查永远不会失败。这种特性被称为“完全安全性”，是比普通安全性强得多的特性。对于任何有趣的编程语言，总的安全性都是不可确定的；然而，像基于集合的分析这样的语义分析可以证明许多在运行时检查的前提条件永远不会失败。此外，对于任何未经证实的前提条件，环境可以构造程序“片段”，识别违反前提条件的执行路径。有了这些信息，程序员就可以决定失败的路径是否可行，如果可行，就修复代码。＊＊＊

9708957 This project will focus on constructing a "smart" programming environment for Java that uses semantic analyses to statically debug, validate, and safely optimize programs. The principal investigators have already developed an early version of such an environment for a dialect of Scheme. A safe implementation prevents the misuse of primitive program operations, such as taking the head of the empty list, through a combination of compile-time analysis, run-time checking, and automatic storage management. Safety, however, is not a panacea: all safe languages defer checking some preconditions until run-time. When a run-time check fails, program execution is aborted. Hence, programmers try to ensure that misapplications are impossible by analyzing what forms of data can appear as input to each primitive operation. Unfortunately, programmers are not very good at this task and frequently make mistakes. The primary goal of the proposed smart programming environment is to prove the run-time checks required for safety never fail. This property, called "total safety," is a much stronger property than ordinary safety. For any interesting programming language, total safety is undecidable; nevertheless, semantic analyses like set-based analysis can prove many of the preconditions checked at run time never fail. Moreover, for any unproven precondition, an environment can construct program "slices" identifying the execution paths violating the precondition. Given this information, the programmer can decide if the failing paths are feasible and, if so, repair the code. ***