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