%0 Conference Paper %1 PavlovicSm03 %A Pavlovic, Dusko %A Smith, Douglas R. %B Formal Methods at the Crossroads: From Panacea to Foundational Support %D 2003 %K ase deductive_program_synthesis inproceedings kestrel overview program_synthesis software_engineering %P 267--286 %T Software Development by Refinement %U http://www.springerlink.com/content/tmf8f6tgfyvgdrvp %V 2757 %X 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 programming concepts, such as algorithm design, and datatype refinement by means of taxonomies of 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. ER -

@inproceedings{PavlovicSm03, 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 programming concepts, such as algorithm design, and datatype refinement by means of taxonomies of 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. ER -}, added-at = {2010-04-21T22:06:18.000+0200}, author = {Pavlovic, Dusko and Smith, Douglas R.}, biburl = {https://www.bibsonomy.org/bibtex/20c985485c7c45fe3626d8bf43e44f7c1/emanuel}, booktitle = {Formal Methods at the Crossroads: From Panacea to Foundational Support}, description = {SpringerLink - Buchkapitel}, interhash = {544edc7b4d8313789a49080aa291dfd7}, intrahash = {0c985485c7c45fe3626d8bf43e44f7c1}, keywords = {ase deductive_program_synthesis inproceedings kestrel overview program_synthesis software_engineering}, pages = {267--286}, series = {LNCS}, timestamp = {2010-04-21T22:06:18.000+0200}, title = {Software Development by Refinement}, url = {http://www.springerlink.com/content/tmf8f6tgfyvgdrvp}, volume = 2757, year = 2003 }