Information Technology Reference
In-Depth Information
2. The claim that proving is too expensive for use in software development also is
false. On the contrary, the economic viability of correctness proving can be
determined on a project-by-project basis using cost-benefit analysis.
3. Despite the claim that correctness proving is too hard, many nontrivial products
successfully have been proven correct, including operating system kernels,
compilers and communication systems. Many tools such as theorem provers
assist in correctness proving. The theorem prover then attempts to prove
mathematically that the product, when given input data satisfying the inputs
specifications, produces output data satisfying the output specifications.
There are some difficulties with correctness proving:
1. How can we be sure that a theorem prover is correct? What reliability can be
placed on the output of a theorem prover? One suggestion is to submit a
theorem prover to it and see whether it is correct.
2. A further difficulty is finding the input and output specifications, and especially
the loop invariance or their equivalents in other logics such as modal logic.
Suppose a product is correct. Unless a suitable invariant for each loop can be
found, there is no way of proving the product correct
3. What if the specifications themselves are incorrect?
Proving product correct is an important, and sometimes vital, software engi-
neering tool. Proofs are appropriate where human lives are at stake or where
otherwise indicated by cost-benefit analysis. Because the aim of software engi-
neering is the production of quality software, correctness proving is indeed an
important software engineering technique. A fundamental issue in execution-based
testing is which members of the software development team should be responsible
for carrying it out.
10.7 Execution-Based Testing
It has been claimed that testing is a demonstration where faults are not present.
Program testing can be a very effective way to show the presence of faults, but it is
hopelessly inadequate for showing their absence. With test data if output is wrong,
then the product definitely contains fault. But if the output is correct, then there
still may be a fault in the product; only information that can deduced from that
particular test is that the product runs correctly on that particular set of test data.
The goal of execution-based testing is therefore to highlight as many faults as
possible while accepting that there is no way to guarantee that all faults have been
detected. A reasonable way to proceed is first to use black-box test cases (testing to
specifications) and then to develop additional test cases using glass-box techniques
(testing to code). The art of black-box testing is to use the specifications to devise a
small, manageable set of test cases to maximize the chances of detecting a pre-
viously undetected fault while minimizing the chances of wasting a test case by
