On a New Notion of Partial Refinement

Emil Sekerinski
(McMaster University)
Tian Zhang
(McMaster University)

Formal specification techniques allow expressing idealized specifications, which abstract from restrictions that may arise in implementations. However, partial implementations are universal in software development due to practical limitations. Our goal is to contribute to a method of program refinement that allows for partial implementations. For programs with a normal and an exceptional exit, we propose a new notion of partial refinement which allows an implementation to terminate exceptionally if the desired results cannot be achieved, provided the initial state is maintained. Partial refinement leads to a systematic method of developing programs with exception handling.

In John Derrick, Eerke Boiten and Steve Reeves: Proceedings 16th International Refinement Workshop (Refine 2013), Turku, Finland, 11th June 2013, Electronic Proceedings in Theoretical Computer Science 115, pp. 1–14.
Published: 24th May 2013.

ArXived at: http://dx.doi.org/10.4204/EPTCS.115.1 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org