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