Program Derivation by Correctness Enhacements

Nafi Diallo
Wided Ghardallou
(FST, Tunisia)
Jules Desharnais
(Laval University, Canada)
Ali Mili

Relative correctness is the property of a program to be more-correct than another program with respect to a given specification. Among the many properties of relative correctness, that which we found most intriguing is the property that program P' refines program P if and only if P' is more-correct than P with respect to any specification. This inspires us to reconsider program derivation by successive refinements: each step of this process mandates that we transform a program P into a program P' that refines P, i.e. P' is more-correct than P with respect to any specification. This raises the question: why should we want to make P' more-correct than P with respect to any specification, when we only have to satisfy specification R? In this paper, we discuss a process of program derivation that replaces traditional sequence of refinement-based correctness-preserving transformations starting from specification R by a sequence of relative correctness-based correctness-enhancing transformations starting from abort.

In John Derrick, Eerke Boiten and Steve Reeves: Proceedings 17th International Workshop on Refinement (Refine'15), Oslo, Norway, 22nd June 2015, Electronic Proceedings in Theoretical Computer Science 209, pp. 57–70.
Published: 4th June 2016.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: