Relational Mathematics for Relative Correctness

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

Braga

Conferencia; 15th International Conference, RAMiCS 2015; 2015

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.