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