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