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