Java Reference

In-Depth Information

{
x > 0
} while
(x > 0) x= x+1;
{
x = 0
}

This triple is
false
. The statement does not terminate in all states in which

the precondition is true.

{true}
x= 1;
{false}

This triple is
false
. The statement is guaranteed to terminate, but when it

does, the postcondition will not be true.

{true} while
(Math.random() != .5)
{false}

This triple is
false
. Termination of the loop is not guaranteed.

Specification of a program segment

We can use the Hoare triple to specify what a program segment —say, a

sequence of statements— is supposed to do. Generally, we also have to say what

variables the program segment may or should change. Here are examples. Each

example specifies the statement by giving a command that says what it should do

and then writes the specification as a Hoare triple.

1. Specification of a statement
S
: Given
y>0
, store
x
y
in
z
. In other words,

write a program segment
S
that satisfies the following Hoare triple, where
S

changes only
z
(
S
may, of course, change local variables declared in it):

{
y≥0
}
S
{
z=x
y
}

2. Specification of a statement
S
: Set
z
to the maximum of
x
and
y
. In other

words, write
S
to store in
z
so that:

{true}
S
{
z = max(x, y)
}

3. Specification of a program
S
: Sort array
b
. The specification:

{true}
S
{
b
is in ascending order
}

is not completely satisfactory because
S
could simply set all elements of array
b

to 0. We could say in English that
S
may only swap elements of
b
. But to place

the requirement that
S
only permute the elements of
b
in the Hoare triple itself,

do the following. First, introduce boolean function
perm(b, B)
with definition:

perm(b, c) =
“array
b
is a permutation of array
c
”

Then, write the Hoare triple as:

{
perm(b, B)
}
S
{
perm(b, B)
and
b
is in ascending order
}

Here,
B
is taken to be a virtual constant —meaning that it cannot be used in state-

ment
S
, so it cannot be changed. The specification says that if
b
is a permutation

of some array
B
, then after execution of
S
, b is still a permutation of
B
and, fur-

thermore,
b
is in ascending order.

4. Specification of a program
S
: Swap
x
and
y
, if necessary, to truthify
x≤y
.

We use two virtual constants
X
and
Y
:

Search WWH ::

Custom Search