University of Washington
Spring 2004
instructor: Rob DeLine
ta: Miryung Kim
due Mon 19 May 2004
This assignment will give you the opportunity to verify software using preconditions and Esc/Java. You are to work alone on this assignment. You may ask your classmates for clarifications about the assignment, but not discuss solutions. You should feel free to consult the course readings, the lecture notes, and general material from the library or internet that describes program verification. You should not consult the library or internet for solutions to these assignment questions or similar questions, since that would rob you of the opportunity to hone your abstraction skills. Finally, please monitor the course mailing list for questions and clarifications about the assignment.
This problem is to use weakest preconditions to prove that the following routine correctly swaps the values of the integer parameters x and y. (Recall that ^ is the logical XOR operator.)
void Swap (ref int x, ref int y)
{
// Let x0 be the initial value of x
// and y0 be the initial value of y.
// C0 holds here
x = x ^ y;
// C1 holds here
y = x ^ y;
// C2 holds here
x = x ^ y;
// Post: x == y0 && y == x0
}
The predicate Post shows the algorithm's final state. Use weakest preconditions to derive state predicates C2, C1, and C0 and show that C0 is equivalent to our initial condition x==x0 and y==y0. As a hint, recall that A ^ A == 0 and A ^ 0 == A.
Use weakest preconditions to show the total correctness of the following routine.
void BubbleSort (int[] a)
{
int outer, inner;
outer = a.length - 1;
while (outer > 0)
{
inner = 0;
while (inner < outer)
{
if (a[inner] > a[inner + 1])
{
Swap(a[inner], a[inner+1]);
}
inner = inner + 1;
}
outer = outer - 1;
}
// Post: forall int i in 0 .. a.length-2 | a[i] <= a[i+1]
}
That is, you are to show that the condition labled Post holds at the end of the code and that the code always terminates. Since we did not discuss how to compute weakest preconditions for procedure calls, you can treat the call to Swap as a primitive operation that has the effect from Problem 1. That is, it obeys the Hoare triple
// a[x] == v0 && a[y] == v1 Swap(a[x], a[y]); // a[x] == v1 && a[y] == v0
In your solution, be sure to highlight the loop invariant and variant function for both of the loops.
First download Esc/Java 2. (Both Miryung and I successfully installed and ran the Linux version, but neither of us had much luck with the Windows/Cygwin version, so I reluctantly recommend that you use Linux.)
The problem starts with the Bag class that you saw in lecture and adds a new constructor and method (add). The code is here. Both the new constructor and the new method contain bugs and lack sufficient specifications for Esc/Java to prove the methods correct. The problem is to change the code and specs until Esc/Java reports no errors. In many cases, there are multiple reasonable ways to deal with a problem that Esc/Java reports, for example, adding a precondition versus adding special cases to the implementation. For each change that you make, write a comment nearby in the code justifying why you believe the change that you're making is the right alternative for fixing the problem.
As with assignment 2, you should hand in your assignment both using E-Submit and on paper in lecture. For the paper copy, please print out all three problems as three separate documents, each of which has your name on in and is stapled together. The three stapled documents should then be paper-clipped together and handed in. This arrangement allows Miryung and I to split up the hand-ins by problem and to grade them in parallel. Your cooperation in this little bit of bureaucracy is greatly appreciated!