Generating Programs plus Proofs by Refinement 1 Technical Approach

We advocate an automated refinement approach to developing programs and their proofs. The approach is partially embodied in the Specware system [6] which has found industrial and government applications. Our view is that the future of software engineering lies in the tight integration of synthesis and analysis processes. Specifications Refinement-oriented development starts with the requirements of the procuring organization. These requirements are typically a mixture of informal and semiformal notations that reflect the needs of the organization. To provide the basis for a clear contract, the requirements must be formalized into specifications that both the procuring organization (the buyer) and the developer (the seller) can agree to. Specifications can be expressed at a variety of levels of abstraction. At one extreme a suitable high-level programming language can sometimes serve to express executable specifications. However, an executable specification requires the inclusion of implementation detail that (1) is time-consuming to develo