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