Java Reference
In-Depth Information
do use them all the time when we develop an invariant for a loop from its spec-
ification and then develop the loop from the invariant, as shown in Chap. 7.
This material necessarily is terse and compact. It is not a tutorial but a brief
summary of the material. For more information, turn to a text like
The Science of
Programming
, by David Gries (Springer-Verlag, 1981).
IV.1
Hoare triples
Recall from Sec. 2.6.2 that an
assertion
is simply a true-false statement placed
before or after a statement in a program, with the intent that it should be true at
that place. An assertion placed before a statement is a precondition of the state-
ment; an assertion placed after the statement is a postcondition of the statement.
For example, consider the following:
{
x=0
}
x= x + 1;
{
x>0
}
In this appendix, we write assertions within bold braces. The field of formal
development of programs uses plain braces { and }, but they cannot be used here
because they already have a meaning in Java. We could place the assertion with-
in comment symbols, but this gets too cumbersome.
Such an assertion-statement-assertion triple is called a
Hoare triple
, after
Tony Hoare, who invented the notation in about 1969. It has this meaning:
Suppose the precondition (in the above case,
x=0
) is true and the
statement (
x= x + 1;
) is executed. Then, execution is guaranteed
to terminate, and when it does, the postcondition (
x>0
) will be
true.
Note that the Hoare triple is itself a true-false statement. We can write false
(or erroneous) ones. Below, we give some Hoare-triples and indicate whether
they are true or not.
{
x=0
}
x= x -
1
;
{
x<0
}
This triple is
true
.
{
x=0
}
x= x -
1
;
{
x
=
0
}
This triple is
false
.
{true} if
(x > y)
Swap
x
and
y
{
x ≤ y
}
This triple is
true
.
{false}
x= 1;
{
x = 0
}
This triple is
true
. In no state is
false
true. Hence, in every state in which
the precondition is true (there are none), execution terminates with the post-
condition true. If the precondition is
false
, the postcondition can be any-
thing.
Search WWH ::
Custom Search