Designware: Software Development by Refinement
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.
KeywordsSoftware Development Design Knowledge Global Search Algorithm Specification Morphism Requirement Acquisition
Unable to display preview. Download preview PDF.
- 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
- 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
- Meseguer, J. General logics. In Logic Colloquium 87, H. Ebbinghaus, Ed. North Holland, Amsterdam, 1989, pp. 275–329.Google Scholar
- 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
- 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
- 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