Recitation 6 - Exercise in Formal Specifications and Program Correctness
Reasoning about correctness of implementation of individual methods is relatively straightforward. The steps are:
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 . c.els[i] is an Integer &&
// for all integers i, j . (0 <= i < j < c.els.size =>
// c.els[i].intValue != c.els[j].intValue)
private Vector els;
// constructors
public IntSet () {
// @effects: Initializes this to be empty.
els = new Vector();
}
// mutators
public void insert (int x) {
// @modifies: this
// @effects: Adds x to the elements of this.
Integer y = new Integer(x);
if (getIndex(y) < 0) els.add(y);
}
// 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 of Java type Integer, and that this is a set (values of elements are unique in the set).
Question:
Does this implementation preserve the rep invariant?
Answer:
The constructor allocates a new empty Vector for els, so the rep invariant holds
for the object returned by the constructor. The observer, size, does not modify
the object, so the rep invariant is preserved for this method. Finally, the
mutator, insert, checks to see if the integer to be added is already represented
in the set. If it is, it does nothing, so the rep invariant is preserved in this
case. If it isn't, it uses the add method, which increments size, so the rep
invariant is preserved for this case also. Therefore, the answer is yes.
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(new Integer(x)) >= 0;
}
Question:
Does this preserve the rep invariant?
Answer:
Yes, it does not modify this.
Suppose now that the following method is added.
public List allEls() {
// @effects: Returns a list containing the elements of this, each exactly once,
// in arbitrary order.
return els;
}
Question:
Answer:
No, because it exposes the rep.
Because the els Vector, which is a member of this, is
returned, the calling method can mutate els directly. For example, it might insert
an element for an integer that is already in the set.
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 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. The calling code would look something like this.
// intSet1 is an IntSet
for (Iterator iter = intSet1.allEls(); iter.hasNext(); ) {
Integer setEl = iter.next();
...
}
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.
Integer y = new Integer(x);
els.add(y);
}
Question:
Answer:
No. It potentially violates the invariant that the values of the elements be
unique.
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
Weakest precondition, expressed as
wp(S,Q)is the weakest predicate 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.
Question:
Suppose S is x = Math.pow(x,y), and Q is x > 0. Suppose that P is x is even, y is odd.
Is the program correct?
Answer:
No. wp(S,Q) = xy > 0
But if y is odd, and x is less than 0 (-2, for example), the weakest predicate
does not hold. In this case, P does not imply wp(S,Q).
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.
Question:
Suppose S1 is x = Math.pow(x,y), S2 is x = Math.pow(x,y), and Q is x >= 0. Suppose that P is x is even, y is odd.
Is the program correct?
Answer:
No.
wp(S1, wp(S2,Q)) = (xy)y >= 0
We know that (xy)y =
x(y2). If y is odd, then y2 is odd.
So if x is negative and y is odd, then the boolean expression will not
hold. Therefore, the weakest precondition is not implied by the
predicate given.
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.
Question:
Suppose the statement is
if (x > 3) {
x = Math.pow((x - 3),y)
} else {
x = Math.pow(x,y)
}
Answer:
Yes.
wp(S,Q) = (x > 3) => (x - 3)y > 0 & !(x > 3) => xy > 0
Given P, this is always true.
Loop Invariants
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.
Question:
Suppose the loop statement is
while (x > y) {
y = y + 1
}
Answer:
Yes. The invariant, I, is that the number of iterations that have already occurred, plus
the number of iterations that still will occur be greater than 3. This can be expressed
as
I = y + (x - y) > 3 = x > 3
Thus, the invariant becomes trivial, and the above conditions are all satisfied.
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;
}
Question:
Answer: "y" works. Your class might suggest others. (If your class asks, an appropriate loop invariant for this example is GCD(a,b) == GCD(x,y))
The situation is not so simple for an entire program, which may contain many classes. How can the state for an entire program be modelled? One way is to use an object model. An object model consists of a graph and a textual description. The graph contains nodes and edges, the nodes representing the kinds of objects in the program, and the edges representing relations between them. Specifically, each node is a named set of instances. The textual description contains definitions of the nodes and relations, and also definitions of derived relations and additional constraints.
Note that, as discussed in lecture, there are code object models and program object models. The examples discussed in this recitation are all program object models.
Consider, for example, a manufacturing scheduling application. The text description for nodes and relations is as follows. Nodes would include:
Thus, an operation consumes one or more resources as the operation begins, and "produces" one or more resources as the operation ends. For example, a dough mixing operation might consume flour, milk, and sugar resources, and might produce a cookie dough resource. It might also require a mixing machine, and a human operator for the operation. These are also modelled as resources; the mixing machine and human operator are "consumed" at the start of the operation, and then "produced" at the finish.
There are some important pieces of information missing from this diagram as it currently exists. Relations should indicate their multiplicity. A relation maps to a set; it maps from a single item in the source set (node) to a set of items in the target set (node). The relation's multiplicity defines how many items are in the set. This is indicated in the diagram by annotating relation arrows with the following symbols:
Exercise:
Fill in the relation annotations in the above diagram.
Answer:
Thus, an operation always has one start time, one finish time, and one duration. It can have zero or more input resource requirements, and one or more output resource requirements (it should have at least one because it is supposed to produce something).
Additional constraints can be added to the text description. For example, the duration will typically depend on the type of operation. Details about what kinds of resources can fulfill a resource requirement will also depend on the type of operation. There may be sequencing constraints between operations (the finish time for DoughMixing should be less than the start time for Baking).
Exercise:
In a scheduling application, it is necessary to assign (match) actual resources with
resource requirements. Extend the object model to include resources and their assignment
to resource requirements.
Answer:
Thus, the role of the scheduling application is to make these resource assignments, subject to constraints (specified in the text description). Additional possible exercises (TA discretion)
Exercise:
Develop an object model for a customer relationship management application.
Nodes would include:
Answer:
[Note to TA's: this is only one possible answer. There might also be relations between company and product, and between company and customer rep. Also, relation names have been omitted from this diagram for the sake of brevity. Make up any names you like.] Additional examples of object models are given in Ch. 12 of the text.