Java Reference

In-Depth Information

{
perm({x, y}, {X, Y})
}
S
{
perm({x, y}, {X, Y})
and
x≤y
}

5. Specification of a program
S
. Print
x
on the Java console, followed by a line

feed. We can write this as a Hoare triple if we use a String variable
javaConsole

(say) to denote the Java console. Again using a virtual constant, we have:

{
javaConsole = JV
}
S
{
javaConsole = JV + x + "\n"
}

This example shows how we can deal with statements that print on the Java con-

sole or some file.

IV.2

Two inference rules

Suppose we know that the following Hoare triple is true:

{
x≥0
}
S
{
y=x
and
z = x+1
}

Then, we can also conclude that statement S does its job in an initial state in

which x = 0 and in a final state in which z = x+1:

{
x=0
}
S
{
y=x
and
z = x+1
}

{
x≥0
}
S
{
z = x+1
}

That is, we can replace the precondition by something that implies it, and we can

replace the postcondition by something that it implies. We might write this as:

{
x = 0
}

{
x ≥ 0
}

S

{
y=x
and
z = x+1
}

{
z = x+1
}

Thus, if we have two adjacent assertions, the rule is that the first must imply the

second, i.e. whenever the first is true, the second must be true too. We might do

something like this if we are interested only in the “stronger” precondition, in

this case
x=0
, or the “weaker” postcondition, in this case,
z = x+1
.

To formalize these notions, we use the logical operator
implication

operation
b => c
, which is defined as follows:

Definition of implication
=>

false
=>
false
is
true

false
=>
true
is
true

true
=>
false
is
false

true
=>
true
is
true

Note: Boolean expression
P
is stronger than boolean expression
Q
if
P
is true in

fewer states than
Q
. We also then say that
Q
is weaker than
P
. Here is a more pre-

cise definition:

Search WWH ::

Custom Search