Software development by refinement

Abstract

This paper presents an overview of the technical foundations and current directions of Kestrel's approach to mechanizing software development. The approach emphasizes machine-supported refinement of property-oriented specifications to code, based on a category of higher-order specifications. A key idea is representing knowledge about pro-gramming concepts, such as algorithm design, and datatype refinement by means of taxonomies of abstract design theories and refinements. Concrete refinements are generated by composing library refinements with a specification. The framework is partially implemented in the research systems Specware, Designware, Epoxi, and Planware. Specware provides basic support for composing specifications and refinements via colimit, and for generating code via logic morphisms. Specware is intended to be general-purpose and has found use in industrial settings. Designware extends Specware with taxonomies of software design theories and support for constructing refinements from them. Epoxi builds on Designware to support the specification and refinement of systems. Planware transforms behavioral models of tasks and resources into high-performance scheduling algorithms. A few applications of these systems are presented. © Springer-Verlag Berlin Heidelberg 2003.