Practical New-Generation Reusable Software Components

这项研究是为了继续先前NSF支持的研究，以解决阻碍软件重用进展的各种技术问题。已经开发了一种全面的重用方法，它允许人们编写可重用组件的正式规范，使用验证和测试来证明它们的正确性，并为它们构建特别有效的实现。这个项目的总体目标是演示新一代正式指定的、经过认证的、高效的可重用软件组件的实用性。具体来说，研究人员打算为通用可重用软件组件的代表性样本设计可理解的形式化规范；展示如何使用这些规范来验证和测试这些模块及其客户端实现的正确性；并应用一些新的数据结构和算法来构建这些组件的有效实现。项目的成功完成将包括其结果(1)具有可证明的正确和有效实现的可重用软件组件的正式规范目录，以及(2)包含以类似方式开发其他可重用组件的明确指导方针的“设计手册”。

This research is to continue prior NSF supported research to address various technical problems that impede progress toward software reuse. A comprehensive approach to reuse has been developed, which permits people to write formal specifications of reusable components, to certify their correctness using both verification and testing, and to build particularly efficient implementations for them. The overall objective of this project is to demonstrate the practicality of a new generation of formally specified, certified, and efficient reusable software components. Specifically, the researchers intend to design understandable formal specifications for a representative sample of general-purpose reusable software components; to show how to use these specifications to verify and to test the correctness of both implementations of these modules and their clients; and to apply several novel data structures and algorithms to build efficient implementations of these components. Successful completion of the project will include among its results (1) a catalog of formal specifications of reusable software components having certifiably correct and efficient implementations, and (2) a "handbook of design" containing explicit guidelines for developing other reusable components in a similar way.