Refining Program Specifications by Automatic Transformation

通过自动转换细化程序规范

• 批准号: 9803880
• 负责人: Richard Kieburtz
• 金额: --
• 依托单位: Oregon Graduate Institute of Science & Technology
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1998
• 资助国家: 美国
• 起止时间: 1998-06-01 至 2000-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9803880&HistoricalAwards=false
• 关键词: Refining; Program; Specifications; Automatic; Transformation

9803880 Productivity benefits and quality improvement have come about as a result of designing and implementing software at ever higher levels of abstraction. So called "executable specifications"-high level functional descriptions of software-represent the current state of language development for software design. However, software is rarely implemented by directly translating such specifications, as the performance of the resulting product is usually poor. To remedy the performance problem without requiring human effort to reprogram a specification as an implementation, the use of program transformation has often been suggested, rewriting the specification according to rules that preserve its meaning but change its form. The technology of transformational improvement has made progress over a span of twenty years. Several functional language compilers now achieve substantial performance gains through the use of source-language transformations. Many improvements remain to be made, however. This research will build on recent and promising results that improve the performance of recursively defined functions by applying transformations based upon their underlying mathematics. Prototype systems have shown the potential of some of these methods, but these systems have never been fully implemented, integrated, or tested. In particular, this research will integrate a variety of known techniques that are expected to work more powerfully in concert than individually. In this project, a prototype transformation system will be extended so that it can be applied to programs written in a core subset of the programming language Standard ML, as well as in CAML, an ML dialect widely used in Europe. The research will help to determine whether high-level transformations can be effective enough in improving the performance of high-level specifications that software designers might quit worrying about many details of programming.***

9803880由于在更高的抽象级别上设计和实现软件，生产力效益和质量改进已经实现。所谓的“可执行规范”--软件的高级功能描述--代表了软件设计语言开发的当前状态。然而，软件很少通过直接翻译这些规范来实现，因为最终产品的性能通常很差。为了在不需要人工重新编写规范作为实现的情况下解决性能问题，经常建议使用程序转换，根据保留其含义但改变其形式的规则重写规范。转化性改进技术经过二十多年的发展，取得了长足的进步。几个函数式语言编译器现在通过使用源语言转换实现了显著的性能提升。然而，仍有许多需要改进的地方。这项研究将建立在最近和有希望的结果的基础上，这些结果通过基于递归定义的函数的基本数学应用转换来提高其性能。原型系统显示了其中一些方法的潜力，但这些系统从未完全实现、集成或测试。特别是，这项研究将整合各种已知的技术，这些技术有望协同工作，而不是单独工作。在这个项目中，原型转换系统将被扩展，以便它可以应用于用编程语言标准ML的核心子集编写的程序，以及在欧洲广泛使用的ML方言CAML。这项研究将有助于确定高级转换在提高高级规范的性能方面是否足够有效，从而使软件设计人员不必担心编程的许多细节。*