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