A correctness proof is a mathematical technique for showing that a product is correct, in other words, that it satisfi es its specifi cations. The technique is sometimes termed verifi -cation . However, as previously pointed out, the term has another meaning within the test-ing context. In addition, verifi cation is also often used to denote all non-execution-based techniques, not only correctness proving. For clarity, this mathematical procedure will be termed correctness proving , to remind the reader that it is a mathematical proof process.
6.5.1 Example of a Correctness Proof
To see how correctness is proven, consider the code fragment shown in Figure 6.4 . The fl owchart equivalent to the code is given in Figure 6.5 . We now show that the code frag-ment is correct—after the code has been executed, the variable s will contain the sum of FIGURE 6.3
Corrected specifi cations for the sort.
Input specification: p : array of n integers, n 0.
Output specification: q : array of n integers such that q[0] q[1] … q[n 1]
The elements of array q are a permutation of the elements of array p, which are unchanged.
168 Part A Software Engineering Concepts
the n elements of the array y. In Figure 6.6 , an assertion is placed before and after each statement, at the places labeled with the letters A through H ; that is, a claim has been made at each place that a certain mathematical property holds there. The correctness of each assertion is now proven.
The input specifi cation, the condition that holds at A before the code is executed, is that the variable n is a positive integer; that is,
A : n ∈ {1, 2, 3, . . .} (6.1) An obvious output specifi cation is that, if control reaches point H , the value of s contains the sum of the n values stored in array y, that is,
H : s y[0] + y[1] + . . . + y[n − 1] (6.2) In fact, the code fragment can be proven correct with respect to a stronger output specifi cation:
H: k n and s y[0] + y[1] + . . . + y[n − 1] (6.3) FIGURE 6.4
A code fragment to be proven correct.
FIGURE 6.5 The fl owchart of Figure 6.4.
int k, s;
int y[n];
k 0;
s 0;
while (k n) {
s s y[k];
k k 1;
}
Yes
No is k n?
k 0
s 0
s s y[k]
k k 1
sch76183_ch06_154-182.indd 168
sch76183_ch06_154-182.indd 168 04/06/10 1:28 PM04/06/10 1:28 PM
A natural reaction to the last sentence is to ask, From where did output specifi cation (6.3) come? By the end of the proof, we hope you have the answer to that question.
In addition to the input and output specifi cations, a third aspect of the proof process is to provide an invariant for the loop. That is, a mathematical expression must be provided that holds at point D irrespective of whether the loop has been executed 0, 1, or many times. The
loop invariant that will be proven to hold is
D: k ⱕ n and s y[0] + y[1] + . . . + y[k − 1] (6.4)
However, the input specifi cation (6.1) holds at all points in the fl owchart. For brevity, the and n ∈ {1, 2, 3, . . .} therefore is omitted from now on.
At point C , as a consequence of the second assignment statement, s R 0, the following assertion is true:
C: k 0 and s 0 (6.6)
Now the loop is entered. It will be proven by induction that the loop invariant (6.4) in-deed is correct. Just before the loop is executed for the fi rst time, assertion (6.6) holds; that FIGURE 6.6
170 Part A Software Engineering Concepts
is, k 0, and s 0. Now consider loop invariant (6.4). Because k 0 by assertion (6.6) and n ⱖ 1 from input specifi cation (6.1), it follows that k ⱕ n as required. Furthermore, because k 0, it follows that k − 1 −1, so the sum in (6.4) is empty and s 0 as re-quired. Loop invariant (6.4) therefore is true just before the fi rst time the loop is entered.
Next, the inductive hypothesis step is performed. Assume that, at some stage during the execution of the code fragment, the loop invariant holds. That is, for k equal to some value k 0 , 0 ⱕ k 0 ⱕ n, execution is at point D , and the assertion that holds is
D: k 0 ⱕ n and s y[0] + y[1] + . . . + y[k 0 − 1] (6.7) Control now passes to the test box. If k 0 ⱖ n, then because k 0 ⱕ n by hypothesis, it follows that k 0 n. By inductive hypothesis (6.7), this implies that
H: k 0 n and s y[0] + y[1] + . . . + y[n − 1] (6.8) which is precisely the output specifi cation (6.3).
On the other hand, if the test is k 0 ⱖ n? fails, then control passes from point D to point E . Because k 0 is not greater than or equal to n, k 0 n and (6.7) becomes
E: k 0 n and s y[0] + y[1] + . . . + y[k 0 − 1] (6.9) The statement s R s + y[k 0 ] now is executed, so from assertion (6.9), at point F, the fol-lowing assertion must hold:
F: k 0 n and s y[0] + y[1] + . . . + y[k 0 − 1] + y[k 0 ]
y[0] + y[1] + . . . + y[k 0 ] (6.10) The next statement to be executed is k 0 R k 0 + 1. To see the effect of this statement, suppose that the value of k 0 before executing this statement is 17. Then the last term in the sum in (6.10) is y[17]. Now the value of k 0 is increased by 1 to 18. The sum s is unchanged, so the last term in the sum still is y[17], which is now y[k 0 − 1]. Also, at point F , k 0 n.
Increasing the value of k 0 by 1 means that if the inequality is to hold at point G, then k 0 ⱕ n.
Therefore, the effect of increasing k 0 by 1 is that the following assertion holds at point G : G: k 0 ⱕ n and s y[0] + y[1] + . . . + y[k 0 − 1] (6.11) Assertion (6.11) that holds at point G is identical to assertion (6.7) that, by assumption, holds at point D. But point D is topologically identical to point G. In other words, if (6.7) holds at D for k k 0 , then it again will hold at D with k k 0 + 1. It has been shown that the loop invariant holds for k 0. By induction, it follows that loop invariant (6.4) holds for all values of k, 0 ⱕ k ⱕ n.
All that remains is to prove that the loop terminates. Initially, by assertion (6.6), the value of k is equal to 0. Each iteration of the loop increases the value of k by 1 when the statement k R k + 1 is executed. Eventually, k must reach the value n, at which time the loop is exited and the value of s is given by assertion (6.8), thereby satisfying output specifi cation (6.3).
To review, given the input specifi cation (6.1), it was proven that loop invariant (6.4) holds whether the loop has been executed 0, 1, or more times. Furthermore, it was proven that after n iterations the loop terminates; and when it does, the values of k and s satisfy the output specifi cation (6.3). In other words, the code fragment of Figure 6.4 has been mathematically proven to be correct.
sch76183_ch06_154-182.indd 170
sch76183_ch06_154-182.indd 170 04/06/10 1:28 PM04/06/10 1:28 PM