Proving Programs Correct Using Plain Old Java Types

Proving Programs Correct Using Plain Old Java Types, by Radha Jagadeesan, Alan Jeffrey, Corin Pitcher, James Riely:

Tools for constructing proofs of correctness of programs have a long history of development in the research community, but have often faced difficulty in being widely deployed in software development tools. In this paper, we demonstrate that the off-the-shelf Java type system is already powerful enough to encode non-trivial proofs of correctness using propositional Hoare preconditions and postconditions.

We illustrate the power of this method by adapting Fähndrich and Leino’s work on monotone typestates and Myers and Qi’s closely related work on object initialization. Our approach is expressive enough to address phased initialization protocols and the creation of cyclic data structures, thus allowing for the elimination of null and the special status of constructors. To our knowledge, our system is the first that is able to statically validate standard one-pass traversal algorithms for cyclic graphs, such as those that underlie object deserialization. Our proof of correctness is mechanized using the Java type system, without any extensions to the Java language.

Not a new paper, but it provides a lightweight verification technique for some program properties that you can use right now, without waiting for integrated theorem provers or SMT solvers. Properties that require only monotone typestates can be verified, ie. those that operations can only move the typestate "forwards".

In order to achieve this, they require programmers to follow a few simple rules to avoid Java's pervasive nulls. These are roughly: don't assign null explicitly, be sure to initialize all fields when constructing objects.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Not Surprising

Types have the same structure as Prolog 'structs', so it is not surprising they can encode proofs. Parametric types or generics are sufficient for this. What's interesting to me is that type-classes provide a sufficient logic to find proofs (although the different instance selection mechanisms affect the power of this, most specific match and backtracking along with type disequality seem to give good results.)

I am not really decided whether SMT style (non-directed) or Prolog style directed search it the best for this. There have been some interesting papers about extending directed search to gain some of the efficiencies present in SMT solvers.

Paper is based on Java 6

Gabrielle Anderson pointed out that the techniques used in the paper rely on not being able to infer solutions to cyclic type constraints. This is true in Java 6, but not in Java 7, so the paper is now a bit of a historic curio.

An example program which shows the difference is, which compiles with JDK 1.7 but not 1.6.