MIT

Problem Set 5: Code Verification (due Wed April 20)

This assignments comprises 3 parts: reading 4 classic papers with study questions, running ESC/Java on a simple program, and working out a simple proof using weakest preconditions.

Reading

These papers are available for download from the private website to which students of the course have access.

  1. C. A. R. Hoare. An Axiomatic Basis for Computer Programming. Volume 12, Issue 10 (October 1969). Pages 576-580. ISSN 0001-0782 ACM Press. New York, NY, USA.

  2. E.W. Dijkstra. EWD472: Guarded commands, non-determinacy and formal derivation of programs. Communications of the ACM 18 (1975), 8: 453-457.

  3. Jon Bentley. Programming Pearls. Addison-Wesley, 1986. ISBN 0-201-10331-1

  4. Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata. Extended Static Checking for Java. Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation. Berlin, Germany, 2002. Pages 234-245. ACM Press. New York, NY, USA. ISBN: 1-58113-463-0.

Study Questions

  1. What now seems dated about Hoare's motivation for this paper?

  2. Why is Euclid's Algorithm natural to write with guarded commands? Sketch out the algorithm in this style. What does it compute?

  3. What does Bentley think about the roles of testing versus verification?

  4. ESC/Java usually gives correct feedback, but it does not make any guarantees. Why is ESC/Java not sound? Why is it not complete?

ESC/Java

ESC/Java is easy to run. You can download pre-compiled versions from either Compaq, its original developer, or from Kind Software, its current developers. The latter supports more platforms (such as Mac) and may be more up-to-date.

Choose one of the following two Java programs and annotate it enough to get it through ESC/Java: courses.java or MyArrays.java. The first is an example developed by John Hatcliff and Matt Dwyer for use in a course on Software Specifications. The second is a pruned version of Java.util.Arrays. The second option is a more realistic example but will require slightly more annotations.

There is ample online documentation available, but here are a few pointers to get started. Annotations are written as comments and must begin with the tokens "//@" and end with a semicolon, ";". There are 5 types of annotations that you will be using: requires, ensures, assert, assume, invariant.

Most of the annotations you write will be requires statements, which add preconditions to procedures. For example, you might write the following right before a method definition:

//@ requires x > 0 ==> y >= 0;

& means "and", | means "or", and ==> means "then". You can use quantification and type comparisons as follows (<: means subtype):

//@ requires \forall int i; i < a.length ==> a[i] = null;
//@ requires \typeof (x) <: \type (Object));

Writing a precondition tells ESC to do 3 things: (a) make sure that the preconditions are sufficient to ensure any post-conditions will be satisfied, (b) make sure that the preconditions prevent out-of-bounds and null pointer exceptions, (c) make sure that all call sites obey the preconditions. You can add postconditions to a procedure by writing an ensures annotation just before the procedure definition.

//@ ensures \result == a | \result == 0;

ESC/Java is neither sound nor complete in general, so you may sometimes get false error reports. ESC is not able to do arbitrarily complex arithmetic -- for example it may not be able to infer that a value is non-negative if that value is produced via numerical computation. In such a case, you would need to add an assume clause:

//@ assume x > 0;

Clearly, you should use assume statements as little as possible.

If you want to check other properties, you can write assert statements. For example, to claim that a pointer p is non-null, you would write the following:

//@ assert p != null;

Lastly, after a variable declaration, you can state an invariant on that variable. For example,

int x = 0; //@ invariant x >= 0;

Proof Exercise

Consider the following procedure which puts a value into an array of key-value pairs at a specified key:

void put( Entry[] a, Key k, Val v) {
    int i = 0;
    while (i < a.length) {
        if (a[i].key = k)
            a[i].val = v
        i = i+1;
    }
}

Assume there is a helper class Entry:

class Entry {
    Key key;
    Val val;
    }

Deduce the weakest precondition that guarantees the following postcondition:

all 0 <= i < a.length() . if (a_0[i].key_0 = k)
          then (a[i].val = 0)
          else (a[i].val = a_0[i].val_0)

key_0, a_0, and val_0 are the values of key, a, and val in the pre-state. Show your proof as a proof outline -- i.e. code annotated/interwoven with assertions (in the style that we summarized Hoare proofs). Examples of weakest precondition proofs can be found in the scanned lecture notes.

What to Hand In

Your solution should include:

Please recall the somewhat exciting submission instructions.