Designware: Software Development by Refinement

  • Douglas R. Smith
Part of the The Kluwer International Series in Engineering and Computer Science book series (SECS, volume 577)


This 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, Designware, 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.


Software Development Design Knowledge Global Search Algorithm Specification Morphism Requirement Acquisition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. Blaine, L., Gilham, L., Liu, J., Smith, D., , and Westfold, S. Planware — domain-specific synthesis of high-performance schedulers. In Proceedings of the Thirteenth Automated Software Engineering Conference (October 1998), IEEE Computer Society Press, pp. 270–280.Google Scholar
  2. Burstall, R. M., and Goguen, J. A.The semantics of clear, a specification languge. In Proceedings, 1979 Copenhagen Winter School on Abstract Software Specification), D. Bjorner, Ed. Springer LNCS 86, 1980.Google Scholar
  3. Meseguer, J. General logics. In Logic Colloquium 87, H. Ebbinghaus, Ed. North Holland, Amsterdam, 1989, pp. 275–329.Google Scholar
  4. Pavlović D. Semantics of first order parametric specifications. In Formal Methods ’99 (1999), J. Woodcock and J. Wing, Eds., Lecture Notes in Computer Science, Springer Verlag. to appear.Google Scholar
  5. Smith, D. R. Constructing specification morphisms. Journal of Symbolic Computation, Special Issue on Automatic Programming 15, 5–6 (May-June 1993), 571–606.MATHGoogle Scholar
  6. Smith, D. R. Toward a classification approach to design. In Proceedings of the Fifth International Conference on Algebraic Methodology and Software Technology, AMAST96 (1996), vol. LNCS 1101, Springer-Verlag, pp. 62–84.Google Scholar
  7. Smith, D. R. Mechanizing the development of software. In Calculational System Design, Proceedings of the NATO Advanced Study Institute, M. Broy and R. Steinbrueggen, Eds. IOS Press, Amsterdam, 1999, pp. 251–292.Google Scholar
  8. Srinivas, Y. V., and Jüllig, R.Specware: Formal support for composing software. In Proceedings of the Conference on Mathematics of Program Construction, B. Moeller, Ed. LNCS 947, Springer-Verlag, Berlin, 1995, pp. 399–422.CrossRefGoogle Scholar

Copyright information

© Springer Science+Business Media New York 2001

Authors and Affiliations

  • Douglas R. Smith
    • 1
  1. 1.Kestrel InstituteUSA

Personalised recommendations