Java Reference

In-Depth Information

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

Search WWH ::

Custom Search