Java Reference

In-Depth Information

P: b[h..i] ≤ x < b[j..k]

We could have replaced
i
instead of
i+1
by
j
and developed the different loop;

trying both, once sees later that the alternative we chose is easier to work with.

Also, at some point, formally, we will need to bound
i
and
j
, and we end up

using as the invariant:

P: b[h..i] ≤ x < b[j..k]
and
h-1≤i<j≤k+1

Developing the invariant using the technique of replacing an expression by a

fresh variable is usually easy, although in some cases it requires practice and

experience to be able to see which expression is the better one to change.

Delete a conjunct

The boolean expression
X
is weaker than, or more general than, the expres-

sion
X&&Y
. If
X&&Y
is the desired postcondition, a possible invariant is the more

general
X
(or the more general
Y
). Here we get the invariant from the postcondi-

tion by deleting a conjunct.

Generally, one decides to delete a conjunct by investigating what it takes to

truthify the conjuncts of the invariant with simple assignments.

For example, consider a linear search for the index of the first value
x
in an

array segment
b[h..k-1]
). The postcondition is:

R: x
is not in
b[h..i-1]
and
(i = k
or
x = b[i])

We can truthify the first conjunct using
i= h;
. We can truthify the second con-

junct by setting i to k, but then the first conjunct will not necessarily be true. We

can delete the second conjunct and use this for the invariant:

P: x
is not in
b[h..i-1]

Here is another example. Suppose we want to find the largest power of
2
that

is at most
N
, for some
N>0
. Here is the postcondition:

R: p
is a power of
2
and
p≤N
and
N < 2*p

The first and second conjuncts are easy to truthify using
p= 1;
. The third is hard-

er to truthify, so we delete it and end up with the invariant:

P: p
is a power of
2
and
p≤N

Here is third example. We want to find the quotient
q
and remainder
r
when

nonnegative
x
is divided by nonzero
y
. The postcondition is this:

R: x = q * y + r
and
0≤r
and
r<y

The first two conjuncts are truthified by
q= 0; r= x;
. Taking the first two con-

juncts as the invariant, we see that the purpose of the loop will be to reduce
r

until the third conjunct is true —of course, while maintaining invariant
P
:

P: x = q * y + r
and
0≤r

Search WWH ::

Custom Search