Java Reference

In-Depth Information

This text is not the place for a full-blown discussion of developing program

and proof hand-in-hand, and we limit ourselves to a few examples. In this appen-

dix, we are trying to show some of the thought processes that could be used to

solve programming problems. Necessarily, we use as examples programs that are

so simple that the methods might not be needed. You may not have thought about

how
you go about writing a program segment; here, you have a chance to think

about and study that process to some extent. See Sec. IV.6 for an example in

which the methodology really helps.

Finding the maximum

We begin with the problem of storing the maximum of two values in a vari-

able, i.e. we write a program segment
S
that satisfies the following specification:

{true}
S
{
R: z = max(x, y)
}

where
R
names the postcondition.

To solve this problem, we have to know what “maximum” means. One way

to define it is to rewrite the postcondition as follows:

R: (z = x && x ≥ y) || (z = y && y ≥ x)

Now, concentrate on
R
and ask yourself what statement might truthify it —per-

haps not in all cases, but at least in some.

There are two obvious answers: the assignments
z= x;
and
z= y;
because,

according to
R
,
z
will equal
x
or
z
will equal
y
. We investigate using the first

assignment. Will it do the job in all required cases? We can see this by
calculat-

ing
the precondition
[z\x]R
of
{
[z\x]R
}
z= x;
{
R
}

[z\x]R

= <
Definition of
R
; perform the substitution
>

(x = x && x ≥ y) || (x = y && y ≥ x)

= <x = x is true; x = y && y ≥ x
equals
x=y>

x≥y || x=y

<
Note that
x=y => x≥y>

= x ≥ y

Therefore, the assignment
z= x;
does the job if and only if
x≥y
. So, we

will need an if-else statement:

if
(x >= y) z= x;

else
?

where we still have to figure out what to do in the case
x<y
.

We can then perform the same kind of process with the second assignment,

z= y;
. However, a mathematician would simply note that, by symmetry, in the

case
y≥x
, the assignment
z= y;
will do. Thus, we end up with the statement:

Search WWH ::

Custom Search