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