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