Section 1.6 Proof of Correctness
85
“Correctness” has a narrower definition here than in everyday usage. A program is correct if it behaves in accordance with its specifications. However, this
does not necessarily mean that the program solves the problem that it was intended to solve; the program’s specifications may be at odds with or not address
all aspects of a client’s requirements. program validation, which we won’t
discuss further, attempts to ensure that the program indeed meets the client’s
original requirements. In a large program development project “program V &
V” or “software quality assurance” is considered so important that a group of
people separate from the programmers is often designated to carry out the associated tasks.
Program verification may be approached both through program testing and
through proof of correctness. program testing seeks to show that particular
input values produce acceptable output values. Program testing is a major part
of any software development effort, but it is well-known folklore that “testing
can prove the presence of errors but never their absence.” If a test run under a
certain set of conditions with a certain set of input data reveals a “bug” in the
code, then the bug can be corrected. But except for rather simple programs,
multiple tests that reveal no bugs do not guarantee that the code is bug-free,
that there is not some error lurking in the code waiting to strike under the right
circumstances.
As a complement to testing, computer scientists have developed a more mathematical approach to “prove” that a program is correct. proof of correctness uses
the techniques of a formal logic system to prove that if the input variables satisfy
certain specified predicates or properties, the output variables produced by executing the program satisfy other specified properties.
To distinguish between proof of correctness and program testing, consider
a program to compute the length c of the hypotenuse of a right triangle, given
positive values a and b for the lengths of the legs. Proving the program correct
would establish that whenever a and b satisfy the predicates a > 0 and b > 0,
then after the program is executed, the predicate a
2
+ b
2
= c
2
is satisfied. Testing such a program would require taking various specific values for a and b,
computing the resulting c, and checking that a
2
+ b
2
equals c
2
in each case.
However, only representative values for a and b can be tested, not all possible
values.
Again, testing and proof of correctness are complementary aspects of program verification. All programs undergo program testing; they may or may not
undergo proof of correctness as well. Proof of correctness is labor-intensive, hence
expensive; it generally is applied only to small and critical sections of code rather
than to the entire program.
assertions
Describing proof of correctness more formally, let us denote by X an arbitrary
collection of input values to some program or program segment P. The actions
of P transform X into a corresponding group of output values Y; the notation
Y = P(X ) suggests that the Y values depend on the X values through the actions
of program P.
A predicate Q(X ) describes conditions that the input values are supposed to
satisfy. For example, if a program is supposed to find the square root of a positive number, then X consists of one input value, x, and Q(x) might be “x > 0.”
85
“Correctness” has a narrower definition here than in everyday usage. A program is correct if it behaves in accordance with its specifications. However, this
does not necessarily mean that the program solves the problem that it was intended to solve; the program’s specifications may be at odds with or not address
all aspects of a client’s requirements. program validation, which we won’t
discuss further, attempts to ensure that the program indeed meets the client’s
original requirements. In a large program development project “program V &
V” or “software quality assurance” is considered so important that a group of
people separate from the programmers is often designated to carry out the associated tasks.
Program verification may be approached both through program testing and
through proof of correctness. program testing seeks to show that particular
input values produce acceptable output values. Program testing is a major part
of any software development effort, but it is well-known folklore that “testing
can prove the presence of errors but never their absence.” If a test run under a
certain set of conditions with a certain set of input data reveals a “bug” in the
code, then the bug can be corrected. But except for rather simple programs,
multiple tests that reveal no bugs do not guarantee that the code is bug-free,
that there is not some error lurking in the code waiting to strike under the right
circumstances.
As a complement to testing, computer scientists have developed a more mathematical approach to “prove” that a program is correct. proof of correctness uses
the techniques of a formal logic system to prove that if the input variables satisfy
certain specified predicates or properties, the output variables produced by executing the program satisfy other specified properties.
To distinguish between proof of correctness and program testing, consider
a program to compute the length c of the hypotenuse of a right triangle, given
positive values a and b for the lengths of the legs. Proving the program correct
would establish that whenever a and b satisfy the predicates a > 0 and b > 0,
then after the program is executed, the predicate a
2
+ b
2
= c
2
is satisfied. Testing such a program would require taking various specific values for a and b,
computing the resulting c, and checking that a
2
+ b
2
equals c
2
in each case.
However, only representative values for a and b can be tested, not all possible
values.
Again, testing and proof of correctness are complementary aspects of program verification. All programs undergo program testing; they may or may not
undergo proof of correctness as well. Proof of correctness is labor-intensive, hence
expensive; it generally is applied only to small and critical sections of code rather
than to the entire program.
assertions
Describing proof of correctness more formally, let us denote by X an arbitrary
collection of input values to some program or program segment P. The actions
of P transform X into a corresponding group of output values Y; the notation
Y = P(X ) suggests that the Y values depend on the X values through the actions
of program P.
A predicate Q(X ) describes conditions that the input values are supposed to
satisfy. For example, if a program is supposed to find the square root of a positive number, then X consists of one input value, x, and Q(x) might be “x > 0.”