Java Reference
In-Depth Information
{
Q
}
S1; S2
{
R
}
where
S1
and
S2
are statements. If we can find an assertion
P
(say) that satisfies
{
Q
}
S1
{
P
}
and
{
P
}
S2
{
R
}
then we know that execution of
S1
begun with
Q
true will terminate with
P
true
and that subsequent execution of
S2
will terminate with
R
true. Hence, we have
the inference rule:
Sequencing rule
: Provided
{
Q
}
S1
{
P
}
,
{
P
}
S2
{
R
}
we conclude:
{
Q
}
S; S2
{
R
}
We give an example of the use of the sequencing rule. In fact, we use it and
the assignment statement rule to prove that the following sequence swaps the
values of x and y:
t= x; x= y; y= t;
Moreover, we prove this fact by starting with the postcondition and computing a
precondition of the sequence, as follows. Consider postcondition
R
:
R: x = X
and
y=Y
where
X
and
Y
are names of virtual constants (they cannot be used in the code).
First, use the assignment rule to compute precondition
P1
in
{
P1
}
y= Y
{
R
}
:
{
P1: x = X
and
t=Y
}
y= t;
{
R: x = X
and
y=Y
}
Now use
P1
as the postcondition for the second statement and compute its pre-
condition
P2
. Finally, use
P2
as the postcondition for the first statement and cal-
culate its precondition:
{
Q: y = X
and
t=Y
}
t= x;
{
P2: y = X
and
t=Y
}
x= y;
{
P1: x = X
and
t=Y
}
y= t;
{
R: x = X
and
y=Y
}
Now use the sequencing rule to eliminate
P1
and
P2
and end up with:
{
Q: y = X
and
t=Y
}
t= x; x= y; y= t;
{
R: x = X
and
y=Y
}
This Hoare triple tells us that the sequence swaps the values of x and
Y
.
Note that we
calculated
the precondition from the sequence of statements
and the postcondition. The precondition was not given to us; we calculated it. In
general, we try to calculate preconditions in this fashion.
Search WWH ::
Custom Search