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