Contents:
As we have seen, Abstract Data Types (ADT's) are a powerful tool for deferring decisions about data structures until they are fully understood. At some point, however, the ADT must be implemented, and the correctness of the implementation must be evaluated. Two useful tools for evaluating this correctness are abstraction functions, and rep invariants. The focus of this discussion will be on rep invariants, and ensuring correctness by preserving rep invariants.
Reasoning about correctness of implementation of individual methods is relatively straightforward. The steps are:
Reasoning about correctness of implementation of an ADT is trickier because you have to consider the entire class, not just individual methods.
An important part of showing that an ADT is implemented correctly is showing that the rep invariant holds for all objects of the class. This is accomplished as follows:
Consider the problem of representing sets of integers. A set requires no repeating elements, so {1 2 3} is a set of integers, and {1 2 2 3} is not. Consider the following IntSet example implementation.
public class IntSet {
// OVERVIEW: IntSets are unbounded, mutable sets of integers
// The rep invariant is
// c.els != null &&
// for all integers i . 0 ≤ i < c.els.size ⇒ c.els[i] is not null &&
// for all integers i, j . (0 ≤ i < j < c.els.size ⇒
// c.els[i].intValue != c.els[j].intValue)
private ArrayList<Integer> els;
// constructors
public IntSet () {
// @effects: Initializes this to be empty.
els = new ArrayList<Integer>();
}
// mutators
public void insert (int x) {
// @modifies: this
// @effects: Adds x to the elements of this.
if (getIndex(x) < 0) els.add(x);
}
// observers
public int size () {
// @effects: Returns the cardinality of this.
return els.size();
}
// private methods
private int getIndex (Integer x) {
// @effects: If x is in this, returns index where x appears, else returns -1
for (int i =0; i<els.size(); i++)
if (x.equals(els.get(i))) return i;
return -1;
}
}
The rep invariant states that els must not be null, that the elements of els are not null, and that this is a set (values of elements are unique in the set).
Suppose now that the following method is added.
public boolean isIn (int x) {
// @effects: Returns true if x is in this else returns false
return getIndex(x) ≥ 0;
}
Suppose now that the following method is added.
public List<Integer> allEls() {
// @effects: Returns a list containing the elements of this, each exactly once,
// in arbitrary order.
return els;
}
One way to avoid this is to return a copy of els. Another is to return an unmodifiable collection. Another way, which is possibly more elegant, is to return an iterator instead of a collection, as in the following implementation.
public Iterator<Integer> allEls() {
// @effects: Returns an iterator for the elements of this.
return els.iterator();
}
The calling application code can then access all the elements via the iterator, but it can't add elements to els directly, so it cannot break the rep invariant.
Note that in certain cases, iterators for collections allow removal of elements. One can argue that this, in some sense, exposes the rep. In this case, however, it does not expose it enough to break the rep invariant. As an alternative, one could define a separate iterator that does not allow removal.
Note also that Integer is an immutable class. This is important here because if it weren't (if it were possible to mutate the value), the rep would be exposed in a way that would allow the calling code to change the value, and possibly violate the rep invariant.
Suppose that the following method were added to IntSet.
public void quickInsert (int x) {
// @modifies: this
// @effects: Adds x to the elements of this.
els.add(x);
}
Given a pre-condition, P, a post-condition, Q, and a sequence of code statements S, correctness is expressed as:
P {S} Q
Total correctness means that if P is true before starting S, S will terminate cleanly in a state satisfying Q. Partial correctness is slightly weaker in that it does not guarantee that S will terminate cleanly. However, if S does terminate cleanly, then the post-state will satisfy Q. Partial correctness is not as good as total correctness, but it is still extremely useful in that it guarantees either a correct outcome, or an outcome that is obviously wrong (an incorrect result will not be mistaken for a correct one).
Weakest precondition, expressed as
wp(S,Q)is the weakest predicate derived from the precondition such that
wp(S,Q) {S} Q
holds. Then, to show
P {S} Q
it is merely necessary to show that
P ⇒ wp(S,Q)
This technique is used to algorithmically convert assertions about programs to logic. Suppose S is a simple assignment statement: x = e.
Then wp(S,Q) is Q with all (free) references to x replaced by e.
Consider the case where S consists of more than one statement
(two, for example). The weakest predicate is now
wp(S1; S2, Q) = wp(S1, wp(S2, Q))
This just says that the weakest pre-condition for S2 becomes the
post-condition for S1.
Consider the case where S is an if statement. The weakest
predicate is:
wp(if b S1 else S2, Q) = (b ⇒ wp(S1, Q)) & (!b ⇒ wp(S2,
Q))
This just says that the weakest precondition corresponds to the one
for S1 if b is true, and the one for S2 if b is false.
if (x > 3) {
x = Math.pow((x - 3),y)
} else {
x = Math.pow(x,y)
}
and suppose that Q is x > 0. Suppose that P is x > 0, y is
even. Is the program correct?
Loop statements: P {while b S} Q
Loops are difficult to evaluate for correctness because they represent an unknown number of paths. Partial correctness can be proven using loop invariants.
Find an invariant I such that:
P ⇒ I
I & b {S} I
(I & !b) ⇒ Q
This just says that the pre-condition must imply the invariant, the
invariant must hold while the loop condition is true, and Q must
hold when the loop terminates.
while (x > y) {
y = y + 1
}
and suppose that Q is y > 3. Suppose that P is x > 5, y <
2. Is the program correct assuming that the loop terminates?
| I | = | (y + (x - y) > 3) |
| = | (x > 3) |
Proving that the loop terminates can be accomplished using a decrementing function. The decrementing function, combined with the loop invariant allows for total correctness proofs of loop statements.
An example of a decrementing function can be found in proving termination for the Euclidean gcd algorithm, as seen in ps1.RatNum.
int gcd(int a, int b) {
int x = a;
int y = b;
while (y != 0) {
int r = x % y;
x = y;
y = r;
}
return x;
}