Relational Mathematics for Relative Correctness

JULES DESHARNAIS; NAFI DIALLO; WIDED GHARDALLOU; MARCELO F. FRIAS; ALI JAOUA; ALI MILI

LECTURE NOTES IN COMPUTER SCIENCE

Springer

Año: 2015 vol. 9348 p. 191 - 208

0302-9743

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 encom- pass non-deterministic programs, or non-deterministic representations of programs; also, we study the mathematical properties of the new defini- tion, most notably its relation to the refinement ordering, as well as its algebraic properties with respect to the refinement lattice.