Static checking java

As a distraction from learning about denotational semantics, I took a look at ESCJava2, which is an extended static checker for Java. ESCJava2 lets you add annotations to your source code which describe invariants and pre/post-conditions which you expect to be true. Then it goes away and tries to verify that they are true. Often, you have to go back and add extra annotations elsewhere (anyone who has const-ified a C++ program knows this feeling). But eventually you get to a point where you can be fairly confident that your program is (statically) free from all sorts of badness – eg. you’ll never try to pop from an empty stack, you’ll never get a null pointer exception.

This is all done declaratively, which makes it much tastier than unit tests.

Does it work? Well, I got out the source code for my trusty java raytracer, which was literally the first java program I ever wrote .. back in 1996 or something. At about 1,000 lines of code, it’s both “real world” enough to act as a decent test case, yet simple enough to grok quickly.

Initially, I had to spend a while adding ‘non_null’ annotations everywhere – every field in every object had that property. Dull, but useful to have it all checked.

Next was various bound-checking stuff. I had an image class with width/height members and a 2d array of pixels. I ‘knew’ that the array was of the right size, but by asserting some invariants to that effect, I could get ESCJava to statically bounds-check all the code that reads/writes pixels. The invariant were moderately complex things like “forall i < height; pixels[i].length == width". These "forall" quantifiers are what makes this approach tastier than unit tests. With unit tests, you have to pick "representative" data points and then trust that you chose well. In the haskell world, QuickCheck is a big step above that. Perhaps ESCJava brings some hint of universal tastiness to Java? Well, except that it didn't work in practise. My key 'raytrace all the pixels' method couldn't be processed by ESCJava. It gave an error which effectively said "the theorem which I'd have to prove to be sure that the code is safe is just too complex". Disappointing, considering that it was little more than some nested loops plus a bit of logic. ESCJava had a few other nice features though. Since my code is old, it the plain old Vector class. ESC can add a 'phantom' elementType field to your vector, which gives you 1.5-like static type checking on pre-1.5 collections. But in the end, the final nail in the coffin was that ESCJava does not support java 1.5+ features. So it doesn't understand generics. Oh well, no use for the real code that I work with. I'd love to have the time to understand this area more deeply. I like this kind of "unsound and incomplete but useful in practise" part of the statically-checked spectrum.