Relational mathematics for relative correctness

Jules Desharnais, Nafi Diallo, Wided Ghardallou, Marcelo F. Frias, Ali Jaoua, Ali Mili

Research output: Chapter in Book/Report/Conference proceedingConference contribution

12 Scopus citations


In earlier work, we had presented a definition of software fault as being any feature of a program that admits a substitution that would make the program more-correct. This definition requires, in turn, that we define the concept of relative correctness, i.e., what it means for a program to be more-correct than another with respect to a given specification. In this paper we broaden our earlier definition to encompass non-deterministic programs, or non-deterministic representations of programs; also, we study the mathematical properties of the new definition, most notably its relation to the refinement ordering, as well as its algebraic properties with respect to the refinement lattice.

Original languageEnglish (US)
Title of host publicationRelational and Algebraic Methods in Computer Science - 15th International Conference, RAMiCS 2015, Proceedings
EditorsWolfram Kahl, Michael Winter, Jose N. Oliveira
PublisherSpringer Verlag
Number of pages18
ISBN (Print)9783319247038
StatePublished - 2015
Event15th International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS 2015 - Braga, Portugal
Duration: Sep 28 2015Oct 1 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other15th International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS 2015

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science


  • Absolute correctness
  • Fault removal
  • Faults
  • Refinement lattice
  • Refinement ordering
  • Relative correctness


Dive into the research topics of 'Relational mathematics for relative correctness'. Together they form a unique fingerprint.

Cite this