Improving Performance With Assertions

一旦编写了程序，就可以静态地(即程序验证)或动态地(即测试)对照其规范进行检查。该项目合并了这些技术，假定断言始终是动态检查的，但优化了尽可能多的检查。因此，程序验证成为代码优化的特例。代码优化和程序验证将通过使用程序组件规范来优化使用它们的程序来联系起来。有规范的程序组件可能比没有规范的程序组件更快，从而鼓励程序员指定它们。该项目还将研究如何提供性能信息，以便程序员可以看到如何添加断言来提高性能，并可以看到组件何时被错误使用。该项目将使用针对类型化SmallTalk的TS编译器和MUAL交互定理证明器。

Once a program has been written, it can be checked against its specification either statically (i.e. program verification) or dynamically (i.e. testing). The project merges these techniques by assuming that assertions are always checked dynamically but optimizing away as many checks as possible. Thus, program verification becomes a special case of code optimization. Code optimization and program verification will be linked by using the specification for program components to optimize the programs that use them. Program components with specifications are likely to be faster than those without, thus encouraging programmers to specify them. The project will also study how to provide performance information so that the programmer can see how to add assertions to improve performance and can see when components are used incorrectly. The project will use the TS compiler for Typed Smalltalk and the mu-ral interactive theorem prover.