A Smart Programming Environment for Java

9708957该项目将专注于构建一个用于Java的“智能”编程环境，该环境使用语义分析来静态调试、验证和安全地优化程序。主要调查人员已经为方案的一种方言开发了这样一个环境的早期版本。通过结合编译时分析、运行时检查和自动存储管理，安全的实现防止了原始程序操作的误用，例如获取空列表头。然而，安全并不是灵丹妙药：所有安全语言都会将某些前提条件的检查推迟到运行时。当运行时检查失败时，程序执行将中止。因此，程序员试图通过分析哪些形式的数据可以作为每个原语操作的输入来确保不会出现错误的应用程序。不幸的是，程序员不太擅长这项任务，经常出错。拟议的智能编程环境的主要目标是证明安全所需的运行时检查永远不会失败。这种财产被称为“完全安全”，是一种比普通安全更强大的财产。对于任何有趣的编程语言，完全安全是无法确定的；然而，语义分析(如基于集合的分析)可以证明在运行时检查的许多前提条件永远不会失败。此外，对于任何未经证实的前提条件，环境都可以构建标识违反前提条件的执行路径的程序“切片”。根据这些信息，程序员可以决定故障路径是否可行，如果可行，则修复代码。***

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