Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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.
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.
Meseguer, J. General logics. In Logic Colloquium 87, H. Ebbinghaus, Ed. North Holland, Amsterdam, 1989, pp. 275–329.
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.
Smith, D. R. Constructing specification morphisms. Journal of Symbolic Computation, Special Issue on Automatic Programming 15, 5–6 (May-June 1993), 571–606.
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.
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.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer Science+Business Media New York
About this chapter
Cite this chapter
Smith, D.R. (2001). Designware: Software Development by Refinement. In: Winter, V.L., Bhattacharya, S. (eds) High Integrity Software. The Kluwer International Series in Engineering and Computer Science, vol 577. Springer, Boston, MA. https://doi.org/10.1007/978-1-4615-1391-9_1
Download citation
DOI: https://doi.org/10.1007/978-1-4615-1391-9_1
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4613-5530-4
Online ISBN: 978-1-4615-1391-9
eBook Packages: Springer Book Archive