Correctness of programs - Multimedia Introduction to Programming Using Java - page 494

Appendix IV
Correctness of Programs
OBJECTIVES
• Outline the basic ideas of proving a sequence of statements correct.
• Outline how to develop a program and its proof hand in hand, with the
proof ideas leading the way.
INTRODUCTION
In this appendix, we show how to specify a program segment in terms of a pre-
condition and postcondition. We then look at how the assignment statement, if-
statement, and loop can be defined —not in terms of how they are executed but
in terms of when a precondition-statement-postcondition triple { Q } S { R } is true.
We discuss how these ideas can be used to develop sequences of statements, with
the proof ideas leading the way.
We use the boolean implication operator => (which will be defined at the
appropriate time). We also introduce the notion of an axiom . An axiom is a basic
true-false statement that we assume to be true —it is a postulate, a theorem
accepted without proof. Also, we will introduce inference rules , which are used
to generate new theorems from old ones.
We confine our attention to the empty statement, the assignment statement,
the conditional statement, and the while-loop.
A major principle is that the task is not to prove an existing program correct
but to develop a program and its proof hand-in-hand —with the proof ideas lead-
ing the way. A second principle is that parts of a program can be calculated , rather
than guessed. Most of our examples are necessarily very simple, in order to
explain the ideas. But see Sec. IV.6 for a real illustration of the power of the
methodology.
While the ideas concerning program correctness may be formal, they can
(and perhaps should) be utilized in an informal manner in most cases. In fact, we