Java Reference
In-Depth Information
IV.3.5
Conditional statements
Consider an if-statement with a pre- and a post-condition:
{ Q }if (B) S { R }
What do we need to know to see that this Hoare triple is true? First, if B is false,
then S is not executed, so R must be true in the initial state. Thus, we have the
premise: Q and B => R . Second, if B is true, execution of S begun with Q and B
true has to make R true, so we have the premise: { Q and B } S { R } . Thus, we
end up with this inference rule concerning the if-statement:
if-rule : Provided Q and B => R , { Q and B } S { R }
we conclude: { Q }if (B) S { R }
You can see that the if-statement rule simply states what any programmer
would have to do to understand that the if-statement does its job. There is noth-
ing magic or special about it. In the same way, we have the following inference
rule for the if-else statement:
if-else-rule : Provided { Q and B } S1 { R }, { Q and !B } S2 { R }
we conclude: { Q }if (B) S1 else S2 { R }
IV.3.6
The while-loop
We now define the while-loop:
{ Q } while (B) S { R }
in terms of an inference rule. We need to develop some premises from which we
can conclude that the above holds. This will require us to use an assertion P ,
which we call the invariant of the loop because it will be true before and after
execution of repetend S. To show this, we annotate the loop as follows:
{ Q }
{ P }
while (B)
{ P && B } S { P }
{ P && !B }
{ R }
From this annotation, we can see that { Q } while (B) S { R } holds under the
following conditions:
1. Q => P
2. { P && B } S { P }
3. P && !B => R
4. The loop terminates
This leads to the following inference rule:

Search WWH ::

Custom Search