Improving Performance With Assertions

通过断言提高性能

• 批准号: 9014576
• 负责人: Ralph Johnson
• 金额: $ 12.39万
• 依托单位: University of Illinois at Urbana-Champaign
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1990
• 资助国家: 美国
• 起止时间: 1990-09-15 至 1993-02-28
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9014576&HistoricalAwards=false
• 关键词: Improving; Performance; Assertions

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.

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