Saturday, March 19, 2011

Unit testing reloaded: Java Path Finder

Unit tests are good. Sometimes we hate them because of the work overhead they require, but almost everyone agree on their usefulness. So the question is: what could we do to eliminate (or at least minimize) this overhead? The answer is quite simple: we should minimize the number of separate unit tests. It is not impossible, since most of the test cases are based on simple assertions, so they can be easily integrated with the source code. In order to do this we need a simple but powerful notation to express the constraints, since assertions scattered across the source statements obscure the code. Annotations are very helpful in this case. We can create annotations for classes and field variables as well as input parameters and return values of operations (we are talking about the design by contract idiom).
Defining annotations is easy, but it is very time consuming to write a processor for the processing of the statements written in these annotations. Fortunately, we do not have to implement anything, we can use the Java Path Finder. Its jpf-aprop module fully supports the design by contract idiom.
JPF is a real multi-purpose tool, and it has a moderate learning curve. Unfortunately, the online documentation is a bit outdated, but there are many publications and examples that can be downloaded from the site, so an average Java programmer can use the tool without difficulties.