Page 393 - Discrete Mathematics and Its Applications

372 5 / Induction and Recursion

5.5 Program Correctness

Introduction

Suppose that we have designed an algorithm to solve a problem and have written a program
to implement it. How can we be sure that the program always produces the correct answer?
After all the bugs have been removed so that the syntax is correct, we can test the program with
sample input. It is not correct if an incorrect result is produced for any sample input. But even if
the program gives the correct answer for all sample input, it may not always produce the correct
answer (unless all possible input has been tested). We need a proof to show that the program
always gives the correct output.
Program verification, the proof of correctness of programs, uses the rules of inference and
proof techniques described in this chapter, including mathematical induction. Because an incor-
rect program can lead to disastrous results, a large amount of methodology has been constructed
for verifying programs. Efforts have been devoted to automating program verification so that it
can be carried out using a computer. However, only limited progress has been made toward this
goal. Indeed, some mathematicians and theoretical computer scientists argue that it will never
be realistic to mechanize the proof of correctness of complex programs.
Some of the concepts and methods used to prove that programs are correct will be introduced
in this section. Many different methods have been devised for proving that programs are correct.
We will discuss a widely used method for program verification introduced by Tony Hoare in
this section; several other methods are also commonly used. Furthermore, we will not develop a
complete methodology for program verification in this book. This section is meant to be a brief
introduction to the area of program verification, which ties together the rules of logic, proof
techniques, and the concept of an algorithm.

Program Verification

A program is said to be correct if it produces the correct output for every possible input.A proof
that a program is correct consists of two parts. The first part shows that the correct answer is
obtained if the program terminates. This part of the proof establishes the partial correctness
of the program. The second part of the proof shows that the program always terminates.
To specify what it means for a program to produce the correct output, two propositions
are used. The first is the initial assertion, which gives the properties that the input values must
have. The second is the final assertion, which gives the properties that the output of the program
should have, if the program did what was intended. The appropriate initial and final assertions
must be provided when a program is checked.

DEFINITION 1 A program, or program segment, S is said to be partially correct with respect to the
initial assertion p and the final assertion q if whenever p is true for the input values
of S and S terminates, then q is true for the output values of S. The notation p{S}q in-
dicates that the program, or program segment, S is partially correct with respect to the initial
assertion p and the final assertion q.

Note: The notation p{S}q is known as a Hoare triple. Tony Hoare introduced the concept of
partial correctness.
Note that the notion of partial correctness has nothing to do with whether a program termi-
nates; it focuses only on whether the program does what it is expected to do if it terminates.
A simple example illustrates the concepts of initial and final assertions.