Program derivation by correctness enhancements

Nafi Diallo, Wided Ghardallou, Jules Desharnais, Ali Mili

Research output: Contribution to journalConference articlepeer-review

1 Scopus citations


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 morecorrect 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.

Original languageEnglish (US)
Pages (from-to)57-70
Number of pages14
JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
StatePublished - Jun 4 2016
Event17th International Workshop on Refinement, Refine 2015 - Oslo, Norway
Duration: Jun 22 2015 → …

All Science Journal Classification (ASJC) codes

  • Software


  • Absolute correctness
  • Correctness enhancement
  • Correctness preservation
  • Program derivation
  • Program refinement
  • Relative correctness


Dive into the research topics of 'Program derivation by correctness enhancements'. Together they form a unique fingerprint.

Cite this