Java Reference

In-Depth Information

if
(x >= y) z= x;

else
z= y;

The astute reader will have noticed that we were not completely formal.

And in general, we do not have to be completely formal. Use just enough for-

mality to be convinced that the result is correct, and the harder the problem the

more formality is needed!

This example brings out two important points. First, it illustrates that
pro-

gramming is a goal-oriented activity
. It is the postcondition that is most impor-

tant at the beginning, not the precondition. The goal, postcondition
R
, was what

we looked at for insight in starting the development.

Second, we were able to
calculate
the if-condition, not guess at it. Of course,

in this case, we could have easily guessed the if-condition, but there are situa-

tions in which calculation is a far better tool than guessing or intuition, which

until now have been the programmers' main tools. In some cases, the methodol-

ogy we are proposing can lead to programs that you would not have thought of

without using the methodology.

Calculating an expression

Consider the following specification for a partially completed multiple

assignment statement:

{
P
}
x, k= E, k+1;
{
P
}

where assertion
P
is:

P: x =
sum of squares of
0..k-1

Note that the precondition and postcondition are the same, and that
k
is being

incremented. We want to know what expression
E
to assign to
x
so that this Hoare

triple is true.We discuss the solution of such problems.

Using the multiple assignment statement axiom, we can place another asser-

tion after the precondition:

{
P
}{
[x,k\E,k+1]P
}
x, k= E, k+1;
{
P
}

Thus, for this to be a true Hoare triple, the following must hold:

P => [x,k\E,k+1]P

We can calculate
E
in (at least) two ways: (1) Assume that
P
holds and massage

[x,k \ E, k+1]P
into a formula for
E
, and (2) Massage
P
until it has the form

[x,k \ E, k+1]P
. Each method has its own situations where it seems easier.

Here, let us try method (2) —the reader should try method (1):

P

= <
Definition of
P>

x =
sum of squares of
0..k-1

= <
Arrange formula so that it contains “sum of squares of

Search WWH ::

Custom Search