Matthew Parkinson verifies Java. Very brief and inaccurate version.

Here are some slides. (His last slide in the first set is ``do David's exercises.'' Obviously, you'll need to know what those were in order to solve them. David's exercises were ``do John's exercises.'' Happy solving!). Here's a summary of the lectures:

• Q: How to model abstraction? A: Use uninterpreted functions.
• Q: How to use separation logic to verify Java programs? A: Use intuitionistic separation logic because it plays well with garbage collection.
• Q: How to deal with inheritance? A: Attach to each method a static spec and a dynamic spec.
• Q: How to reason about concurrency? A: Use a mix of separation logic and rely/guarantee reasoning; we'll call it deny/guarantee.

Do you want more? OK, here's one example. The Visitor pattern is used often by people who write compilers. When you write a.f(b, c) you call function f with three parameters. The first one, a is special in two ways: (1) it will be known by the special name this in the body in of the function and its dynamic type is used to decide which of the functions named f will be called; in general, more than one function f may be called by the same statement depending on the value of a. The Visitor pattern is a work-around not having multiple dynamic dispatch aka multimethods. Or, depending where you come from, you might see it as a work-around not having pattern matching. The main tool used by this pattern is (single) dynamic dispatch, so it will also illustrate how to annotate programs that use this feature of Java.

interface Ast { Ast accept(Visitor v); }
class Constant implements Ast {
  int value;
  @Override Ast accept(Visitor v) { return v.visit(this); }
}
class Plus implements Ast {
  Ast left, right;
  @Override Ast accept(Visitor v) { return v.visit(this); }
}

interface Visitor {
  Ast visit(Constant n);
  Ast visit(Plus n);
}

Given this boilerplate we can do something `useful' to the AST.

class ZeroRemover implements Visitor {
  @Override Ast visit(Constant n) { return n.value == 0? null : n; }
  @Override Ast visit(Plus n) {
    n.left = n.left.accept(this);
    n.right = n.right.accept(this);
    if (n.left != null && n.right != null) return n;
    return n.left != null? n.left : n.right;
  }
}

If you are unfamiliar with the Visitor pattern you can spend a few minutes starring at the code above. Or you could continue reading and notice how sprinkling annotations actually helps to understand the code. So, how do we annotate the accept method? If the visitor and the AST node are OK (for some definition of OK depending on the visitor and on the node, respectively), then some value will be returned (for some definition of some, depending on the particular visitor. OK, so we'll just say what we just said.

interface Ast {
  Ast accept(Visitor v)
    requires this.OK(t) ** v.OK(o)
    ensures v.Result(result, this, t, o);
}

``Whooooaa, stop! What's the funny **, and what are t and o? You said you'll write exactly what you said!'' Uhm, the stars are just the separating conjunction; we use two because one is taken by multiplication. The t and o is just stuff, uninterpreted for now if you want. We're just saying that the Result may depend on the state of the node and on the state of the visitor. Feel better? Yes? OK, then let's move on, it's late. I'll skip some specs so we can move quickly to the next interesting bit. How do we say what ZeroRemover is supposed to do? We just provide a definition for the Result predicate, which was uninterpreted (or `abstract') until now.

class ZeroRemover implements Visitor {
  spec
    Result(r, a, t, o) = r == rz(t);
    plus(Constant(0), x) = x;
    plus(x, Constant(0)) = x;
    plus(x, y) = Plus(x, y);
    rz(Plus(x, y)) = plus(rz(x), rz(y));
    rz(x) = x;

  @Override Ast visit(Constant n) { return n.value == 0? null : n; }
  @Override Ast visit(Plus n) {
    n.left = n.left.accept(this);
    n.right = n.right.accept(this);
    if (n.left != null && n.right != null) return n;
    return n.left != null? n.left : n.right;
  }
}

Let's recap: In the specs you write a Haskell program that does the same thing but is shorter and (perhaps) slower and also some bridges between Haskell (aka math) and your program. As a result you can run a tool to tell you if your efficient(?) Java program does the same thing as the Haskell one.

Now, can you fill in the specs that I skipped? If not, then please do ask in the comments what information you feel you are missing.