Design ware: Software Development by Refinement

AbstractThis paper presents a mechanizable framework for software development by refinement. The framework is based on a category of higher-order specifications. The key idea is representing knowledge about programming concepts, such as algorithm design, datatype refinement, and expression simplification, by means of taxonomies of specifications and morphisms.The framework is partially implemented in the research systems Specware, Design-ware, 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. Planware builds on Designware to provide highly automated support for requirements acquisition and synthesis of high-performance scheduling algorithms.The work reported here is the result of extended collaboration with my colleagues at Kestrel Institute. I would particularly like to acknowledge the contributions of David Espinosa, LiMei Gilham, Junbo Liu, Duško Pavlović, and Stephen Westfold. This research has been partially supported by the US Air Force Research Lab, Rome NY, and by the Defense Advanced Research Projects Agency