Relative correctness is the property of a program to be morecorrect than another with respect to a specification. Whereas traditionally we distinguish between two categories of candidate programs, namely correct programs and incorrect programs, relative correctness arranges candidate programs on a partial ordering structure, whose maximal elements are the correct programs. Also, whereas traditionally we deploy proof methods on correct programs to prove their correctness and we deploy testing methods on incorrect programs to detect and remove their faults, relative correctness enables us to bridge this gap by showing that we can deploy static analytical methods to an incorrect program to prove that while it may be incorrect, it is still more-correct than another. We are evolving a technique, called debugging without testing, in which we can remove a fault from a program and prove that the new program is more-correct than the original, all without any testing (and its associated uncertainties/ imperfections). Given that there are orders of magnitude more incorrect programs than correct programs in use nowadays, this has the potential to expand the scope of proving methods significantly. Also, relative correctness has other broad implications for testing and proving, which we briefly explore in this paper.
Relative correctness is the property of a program to be more-correct than another with respect to a given specification; intuitively, a program P ′ is more-correct than a program P with respect to a specification R if and only if P ′ behaves according to R more often than P , and violates R less egregiously (i.e. in fewer ways) than P . Whereas traditionally we distinguish between two categories of candidate programs for a given specification R, namely correct programs and incorrect programs, relative correctness enables us to arrange candidate programs over a partial ordering structure, whose maximal elements are the correct programs, and all non-maximal elements are incorrect.
Also, traditionally, proving methods and testing methods have been used on different sets of programs: – Proving methods are deployed on correct programs to prove their correctness; they are of limited use when deployed on incorrect programs because even when a proof fails, we cannot always conclude that the program is incorrect, since we cannot tell whether the proof failed because the program is incorrect or because it was improperly documented (re: invariant assertions, intermediate assertions, etc). Some methods of program analysis can identify sources of faults when the correctness proof fails, but their scope is limited. – Testing methods are deployed on incorrect programs to detect, locate and remove their faults; they are useless when deployed on correct programs, because no matter how often a program runs failure-free under test, we can never (in practice) conclude with certainty that it is correct.
We argue that consideration of relative correctness has the potential to alter the
practice of proving methods and testing methods:
– Once we have a formal definition of relative correctness, we can deploy
proving methods to an incorrect program to prove that while it may be incorrect,
it is still more-correct than another. Given that there are orderes of
magnitude more incorrect programs than correct programs, the ability to apply
proving methods to incorrect programs expands the scope of these methods
significantly. This approach is discussed in section 4.
– Relative Correctness can also alter the practice of software testing by
recognizing the difference between testing for relative correctness and testing
for absolute correctness. When we remove a fault from a program, we ought
to test it for relative correctness rather than absolute correctness, unless we
have reason to believe (how do we ever?) that the fault we have just removed
is the last fault of the program. This matter is discussed in section 5.
– It has long been a cornerstone of software engineering wisdom that programs
should not be developed then checked for correctness, but should instead
be developed hand-in-hand along with their proof, with the proof leading
the way [
In section 2 we introduce the mathematical background that is needed to carry out our discussions, and in section 3 we introduce our definition of relative correctness for deterministic and non-deterministic programs. Also, we conclude in section 7 by summarizing our findings, discussing related work, and sketching future directions of research. 2 2.1
In this paper we use relations to represent specifications and programs, hence
we devote this section to discussing some operations and properties of relations.
We assume the reader familiar with elementary relational algebra [
x: X; y: Y; then we mean to let S be the cartesian product S = X × Y ; elements of S are usually denoted by s and the X - (resp. Y -) component of s is denoted by x(s) (resp. y(s)). When no ambiguity arises, we may write x for x(s), and x′ for x(s′), etc. A relation R on set S is a subset of S × S. Special relations on S include the universal relation L = S × S, the identity relation I = {(s, s)|s ∈ S} and the empty relation φ = {}. Operations on relations include the set theoretic operations of union (∪), intersection (∩), difference (\) and complement (R); they also include the converse of a relation R defined by Rb = {(s, s′)|(s′, s) ∈ R}, the domain of a relation defined by dom(R) = {s|∃s′ : (s, s′) ∈ R}, the range of a relation defined by rng(R) = dom(Rb), and the product of two relations R and R′ defined by: R ◦ R′ = {(s, s′)|∃s′′ : (s, s′′) ∈ R ∧ (s′′, s′) ∈ R′}; when no ambiguity arises, we may write RR′ for R ◦ R . ′
A relation R is said to be reflexive if and only if I ⊆ R, symmetric if and only if R = Rb, antisymmetric if R ∩ Rb ⊆ I, asymmetric if and only if R ∩ Rb = φ and transitive if and only if RR ⊆ R. A relation R is said to be total if and only if I ⊆ RRb and deterministic if and only if RbR ⊆ I. A relation R is said to be a vector if and only if RL = R; vectors have the form R = A × S for some subset A of S; we use them as relational representations of sets. In particular, note that RL can be written as dom(R) × S; we use it as a relational representation of the domain of R. 2.2
Given a program p on space S written in a C-like notation, we define the function of p (denoted by P ) as the function that p defines on S, i.e. the set of pairs (s, s′) such that if program p starts execution in state s it terminates in state s′; we may, when no ambiguity arises, refer to a program and its function by the same name, P . Because our discussion of correctness and relative correctness refers to a notion of refinement, we give here a definition of this property. Definition 2.1. Given two relations R and R′, we say that R′ refines R (abbrev: R′ ⊒ R or R ⊑ R′) if and only if RL ∩ R L ∩ (R ∪ R ) = R. ′ ′ Intuitively, this definition means that R′ has a larger domain than R and that on the domain of R, R′ assigns fewer images to each argument that does R. See Figure 1. We use refinement to define correctness.
-: 1 1 XXXXXXz- 2 1 XXXXXXz- 2 2 XXXXXXz- 3 2 XXXXXXz 3 3 3
- 0 : 0 0 XXXXXXz- 1
R′
Fig. 1. R′ ⊒ R Definition 2.2. A program p on space S is said to be correct with respect to specification R on S if and only if its function P refines R.
This definition is identical (modulo differences of notation) to traditional
definitions of total correctness [
Proposition 3.1. Due to [
Definition 3.2. Due to [
To contrast relative correctness with the definition of correctness given in Definition 2.2, we may refer to the latter as absolute correctness. We refer to the domain of (R ∩ P ) as the competence domain of P with respect to R; for deterministic programs, to be more-correct simply means to have a larger competence domain. See Figure 2; note that P ′ is more-correct than P but does not duplicate the correct behavior of P .
In [
: 1
3 1 XXXXXXXz 2
3 1 2 3 : 1 : 2 3 – Ordering Properties. Relative correctness is reflexive and transitive, but not antisymmetric (i.e. two candidate programs could be equally correct, yet compute distinct functions). As a very simple example, consider R defined by R = {(0, 0), (1, 0), (1, 2)} and let P and P ′ be defined by P = {(0, 1), (1, 0)}, P ′ = {(0, 2), (1, 2)}. – Relative correctness culminates in absolute correctness. A (absolutely) correct program is more-correct than (or as correct as) any candidate program. – Relative Correctness Implies Enhanced Reliability. If P ′ is more-correct than P with respect to R, then it is more reliable than P ; but more-reliable is not equivalent to more-correct, as the latter is a logical property whereas the former is a stochastic property. – Relative Correctness and Refinement. Program P ′ refines program P if and only if P ′ is more-correct than P with respect to any specification R. We write this property as:
P ′ ⊒ P ⇔ (∀R : P ′ ⊒R P ). 3.2
In this section we generalize the definition of relative correctness to non-deterministic
programs, as provided by [
Definition 3.3. Given a specification R and two programs P and P ′. We say that P ′ is more-correct than P with respect to R if and only if: (R ∩ P ′)L ⊇ (R∩P )L and (R∩P )L∩R∩P ′ ⊆ P . Also, we say that P ′ is strictly more-correct than P with respect to R if and only if at least one of the inequalities in this definition is strict. Interpretation: The first clause provides that P ′ has a larger competence domain than P . To understand the second clause, consider that the left-hand side of this clause represents the set of (s, s′) pairs such that s is in the competence domain of P (re: (R ∩ P )L) and s′ is an image of s by P ′ that violates specification R (re: R ∩ P ′). What this clause is providing is that any such (s, s′) pair is in P ; so that on the competence domain of P , P ′ does not violate specification R unless P does (but P may violate R in ways that P ′ does not). In other words: P ′ is more-correct than P with respect to R if and only if P ′ has a larger competence domain (first clause), and violates R in fewer ways (second clause). See Figure 3: The competence domain of P is {1, 2} and that of P ′ is {1, 2, 3}. Program P ′ violates R by assigning 1 to 1 and 2 to 2; but P is guilty of the same misdeed, in addition to also assigning 0 to 2 and 3 to 1, in violation of specification R. Hence P ′ is more-correct than P with respect to R.
R
-: 0 0
: 1
3
P 0 XXXXXX-Xz 1
* 0 12 HXXHXXHXXHXXHXXHXXHj-XzXz 23 3 0 1 2 3 Our study of relative correctness came about when we attempted to answer the question: what is a fault in a program? and when can we say that we have removed a fault from a program? The first matter we have to consider is that any definition of a fault must refer to a level of granularity at which we want to isolate faults. The coarsest level of granularity would be to consider the whole program as a possible fault, but that is clearly unhelpful as far as diagnosing and removing faults; more typical levels of granularity include a line of code, a lexeme, an expression, an assignment statement, elementary programming statements, etc. We use the term feature to refer to any part of the source code at an appropriate level of granularity, including non-contiguous parts.
Definition 4.1. Due to [
The analysis of while loops by means of invariant relations provides a way to infer
the relative correctness of iterative programs from partial semantic information.
In [
ID Data
int x; 1R1 const int a>0; x=x+a
float x, y; x=x+a, 2R1 const float a, b; y=y+b
Statements Invariant Relation Pattern {(s, s′)|x mod a = x′ mod a} {(s, s′)|ay − bx = ay′ − bx′}.
Invariant relations are important for our purposes because they enable us to
determine whether a loop is correct or not with respect to a specification, as
shown in the following two propositions (which are due to [
Proposition 4.2. Necessary condition of correctness. Let w be a while loop of the form w = while (t) {b} that terminates for all states in S, let V be an invariant relation for w, and let R be a specification on S. If w is correct with respect to R then (R ∩ V )T = RL.
This proposition provides, in effect, that any while loop that admits an invariant relation V that fails to meet this condition could not possibly be correct with respect to R. We say about such an invariant relation V that it is incompatible with the specification R. Any invariant relation that is not incompatible with the specification is said to be compatible. Proposition 4.3. Sufficient condition of correctness. Given a while loop w of the form while (t) {b} that terminates for all states in its space S, and given a specification R on S, if an invariant relation V of w satisfies the condition
V T ∩ RL ∩ (R ∪ V ∩ Tb) = R then w is correct with respect to R.
This proposition provides, in effect, that if an invariant relation V meets this condition, then it contains sufficient information to subsume the specification, and to prove the correctness of the loop with respect to R. 4.3
While in the previous section we show how invariant relations can be used to
prove the (absolute) correctness or incorrectness of a loop with respect to a
specification, in this section we explore how they can be used to prove relative
correctness of a loop over another with respect to a given specification. A
proposition given in [
As an illustration of this approach, we consider the following example, which
we borrow from [
else other=other+1;}} We find the following invariant relations of this while loop, where σ1 and σ2 designate the set of characters whose Ascii codes are less than, and (respectively) greater than equal to, the code of ’0’: – V0 = {(s, s′)|q = q′} – V1 = {(s, s′)|i ≤ i′} – V2 = {(s, s′)|dig ≤ dig′} – V3 = {(s, s′)|other ≤ other′} – V4 = {(s, s′)|let ≥ let′} – V5 = {(s, s′)|let − #a∪A(q[i..l − 1]) = let′ − #a∪A(q′[i′..l − 1])} – V6 = {(s, s′)|dig + #σ1(q[i..l − 1]) = dig′ + #σ1(q′[i′..l − 1])} – V7 = {(s, s′)|other + #σ2∪ϑ(q[i..l − 1]) = other′ + #σ2∪ϑ(q′[i′..l − 1])} The following table shows which of these invariant relations are compatible, and which are incompatible.
Compatible Invariant Relations Incompatible Invariant Relations V0, V1, V2, V3 V4, V5, V6, V7 Becuse the incompatible column is non-empty, we conclude that the program is incorrect with respect to R, hence we must enhance its correctness. To this effect, we select the incompatible invariant relation V4 for remediation, which leads us to focus on variable let for fault removal. Preservation of the compatible invariant relations mandates that let be modified under the following condition: let ≤ let′. We propose: let=let+1;. The generation of invariant relations of the new loop yields the following table:
Compatible Invariant Relations Incompatible Invariant Relations V0, V1, V2, V3, V4′, V5′ V6, V7 Application of the same process one more time yields the following program: {i=0; let=0; dig=0; other=0; l=strlen(q); while (i<l) {c = q[i];i++; if (A<=c && Z>=c) let=let+1; else if (a<=c && z>=c) let=let+1; else if (0<=c && 9>=c) dig=dig+1; else other=other+1;}} Analysis of this program produces 8 invariant relations, which are all compatible.
Compatible Invariant Relations Incompatible Invariant Relations V0, V1, V2, V3, V4′, V5′, V6′, V7′ This does not prove that the program is now correct, all it proves is that we have no evidence (in the forms of an incompatible invariant relation) that it is incorrect. To establish correctness, we must ensure that the intersection of all the compatible invariant relations satisfies the sufficient condition provided by Proposition 4.3, which it does. All the faults have been removed; we now have a correct program. 5
The usual process of software debugging proceeds as follows: We observe a failure of the program; we analyze the failure and formulate a hypothesis on its cause; we modify the source code on the basis of our hypothesis; and finally we test the new program to ensure that it is now correct. But there is a serious flaw in this process: when we remove a fault from an incorrect program, we have no reason to expect the new program to be correct, unless we know (how do we ever?) that the fault we have just removed is the last fault of the program; hence when a fault is removed from a program, the new program ought to be tested for relative correctness over the original program, rather than for absolute correctness. Of course, regression testing is supposed to ensure monotonicity of fault removal, but regression testing is essentially a test data selection matter, whereas the difference between testing for relative correctness and testing for absolute correctness involves other aspects. We argue that testing a program for relative correctness has an impact on three aspects of testing, namely test data selection, test oracle design, and test coverage assessment.
– Test data selection. The problem of test data selection can be summarized
as follows: We are given a large or infinite test space S, and we must select
a small subset thereof T such that the behavior of candidate programs on
T is a faithful predictor of their behavior on S. The difference between
absolute correctness and relative correctness is that for absolute correctness
with respect to specification R, the test space S is dom(R) whereas for
relative correctness over P with respect to R the test space S is dom(R ∩ P ).
– Test oracle design. Let Ω(s, s′) be the test oracle for absolute correctness
derived from specification R. Because relative correctness over program P
tests a candidate program P ′ for Ω only for those states on which P is
successful, the oracle for relative correctness ω(s, s′) can be written as:
ω(s, s′) ≡ (Ω(s, P (s)) ⇒ Ω(s, s′)).
– Test Coverage Assessment. It is not sufficient to know that some program
P ′ has executed successfully on a test data set of size N using oracle ω(s, s′);
it is also necessary to know what percentage of the test data set satisfy the
precondition Ω(s, P (s)) (i.e. is P ′ more-correct than P because P ′ is very
good or because P is very bad?).
To illustrate the difference between absolute correctness and relative correctness,
we consider the same program as section 4, and we resolve to remove its faults
not by static analysis, as we did there, but by testing for relative correctness after
each fault removal. To this effect, we proceed iteratively as follows, starting from
the original program:
1. Using muJava [
We invoke muJava with the option of mutating statements and conditions and we test every mutant for relative correctness, strict relative correctness and absolute correctness using randomly generated test data of size 1000. Every invokation of muJava generates exactly 64 mutants, which we label by indices 1 through 64; hence for example m4.53.8 is mutant 8 of mutant 53 of mutant 4 of the original program. The outcome of this experiment is shown in Figure 4. The arcs represent relative correctness relationships; at the bottom of this graph is the original program, and at the top is the corrected version of the program. Note that the test for absolute correctness kept coming empty-handed every time except whenever muJava produced the correct program P ′. i.e. six times. The test for relative correctness returned true for every arc in Figure 4 i.e. 25 times; it enabled us to remove faults one at a time, until we reach a correct program. Note also that many mutations prove to be perfectly commutative; such is the case for 4, 8 and 53. Note further that, if we assume for the sake of argument that our test is exhaustive, then the number of arcs emerging from each program represents the number of faults in that program. For example, program P has four faults even though it is three fault removals away from being correct; we say that P has a fault density of 4 and a fault depth of 3. 6
For all its interest, program verification is really a dubious bargain: the idea that
we write programs in an informal/ approximate manner then try to prove their
correctness is not very sound. What is more rational is to seek means to write
programs that are certified to be correct by construction [
m51.8.53 = m51.53.4
= m51.53.8 m4 Qk
Q
Q
Q m8 Q
KA A
A Q A
QA
P
– Preserve correctness, achieve program quality. Starting from the
specification, we transform it progressively to make it more and more program-like,
while preserving correctness through refinement. This is the traditional
process of program construction by successive refinements.
– Preserve program quality, achieve correctness. Starting from the trivial
program abort, we transform it progressively to make more and more-correct
with respect to R until it is correct. In [
We illustrate this process on a program that computes the number of alphabetic characters, numeric characters, and special symbols in an input string. We consider the same space and relation as those given in Section 4, and we present a sequence of programs P0 ... P4 that are increasingly more-correct, though not increasingly more-refined. We do not have a methodology for how to do this in general, hence we merely present the programs and their competence domains. P0 {abort}. CD0 = φ.
P1 {i=0; let=0; dig=0; other=0; l=strlen(q); while (i<l) { c = q[i]; i++;
if (’A’<=c && ’Z’>=c) let+=1;}}
CD2 = {s|q ∈ listhαAi}.
P2 {i=0; let=0; dig=0; other=0; l=strlen(q); while (i<l) {c = q[i]; i++; if (’A’<=c && ’Z’>=c) let+=1; else if (’a’<=c && ’z’>=c) let+=1;}}
CD2 = {s|q ∈ listhαA ∪ αai}.
P3 {i=0; let=0; dig=0; other=0; l=strlen(q); while (i<l) {c = q[i]; i++; if (’A’<=c && ’Z’>=c) let+=1; else if (’a’<=c && ’z’>=c) let+=1; else if (’0’<=c && ’9’>=c) dig+=1;}}
CD3 = {s|q ∈ listhαA ∪ αa ∪ νi}.
P4 {i=0; let=0; dig=0; other=0; l=strlen(q); while (i<l) {c = q[i]; i++; if (’A’<=c && ’Z’>=c) let+=1; else if (’a’<=c && ’z’>=c) let+=1; else if (’0’<=c && ’9’>=c) dig+=1; else other+=1;}
CD4 = {s|q ∈ listhαA ∪ αa ∪ ν ∪ σi}.
Clearly, we do have P0 ⊑R P1 ⊑R P2 ⊑R P3 ⊑R P4; also, we find CD4 = dom(R), hence (by Proposition 3.1) P4 ⊒ R, i.e. P4 is correct with respect to R.
This process bears a striking resemblance to test driven derivation (TDD)
[
In [
– Impact on Proving. Whereas traditionally proving methods are deployed
exclusively on correct programs to prove their correctness, we argue that
relative correctness enables us to apply proving methods to an incorrect program
to prove that despite being incorrect, it is still more correct than another.
Given that there are orders of magnitude more incorrect programs than
correct programs, this points to a potential expansion of the scope of static
analysis methods.
– Impact on Testing. We argue that when we remove a fault from a program
we ought to test it for relative correctness rather than absolute correctness;
of course regression testing is an attempt to test for relative correctness
through the selection of targeted test data, but we argue that testing for
relative correctness has an impact not only on test data selection, but also
on oracle design and test coverage assessment.
– Impact on Program Derivation. Whereas the traditional paradigm of
program derivation is to proceed by successive correctness-preserving
transformations on the basis of refinement, we argue that it is also possible to proceed
by successive correctness-enhancing transformations on the basis of relative
correctness. One of the main advantages of our paradigm is that it models
not only the derivation of programs from scratch, but also many aspects of
software evolution. Given that more software is produced by evolution than
from scratch, this approach carries significant potential in practice.
Other authors have introduced similar-sounding but distinct concepts of relative
correctness [
Whereas most other authors approximate while loops by unrolling them a number of times, we approximate them by means of invariant relations. We view the contrast between unrolling a loop and capturing its behavior by invariant relations as a choice between capturing all the functional details of a few iterations, and capturing some functional detail of all the iterations. We argue that capturing all the functional details is typically unnecessary (not all the loop’s functional properties are worthy / relevant), and modeling a limited number of iterations is typically insufficient (the behavior of the loop for a limited number of iterations may not indicate its behavior for an arbitrary number thereof). Acknowledgement The authors are very grateful to the anonymous reviewers for their thoughful, valuable feedback.