Jon's Assertion Package is tool that allows the use of Design by Contract with Java. The source is up on github.
The basic idea of Design by Contract is that someone can write a piece of code with a particular usage in mind and can then document the usage and then enforce this during development and remove these checks when releasing production code. This is accomplised by using inline assertions, just like assert.h in C, pre conditions, post conditions and invariants. Each condition is a boolean statement that "asserts" that something is true when a piece of code is being executed. Pre conditions assert that a condition is true at the start of execution of a method. Post conditions are for a condition being true at the end of a method. Invariants are conditions that must be true for before and after all public methods in a class are called, in the case of this tool all methods that aren't private. These conditions are also inherited so that someone can define conditions for use of a superclass and all subclasses follow this as well. The way that this is done is by evaluating all of the conditions for a method on one class then either AND or OR this result with the next class in the inheritance tree depending on the type of assertion so that the burden is placed on the person using the method rather than the person writing the method. The following table shows the rules.
| Type of assertion | Logical operation performed for inherited conditions |
|---|---|
| invariant | AND |
| precondition | OR |
| postcondition | AND |
You can find a deeper explanation of DBC in this PDF. The full book that the chapter came from may be found here
The syntax of DBC conditions is pretty simple. The general form is this:
@tag (Java boolean expression), "message";
Where tag is one of pre, post,
assert or invariant. The ', "message";' is
optional. This is used to specify some extra information that will
go into the message that the user sees if the condition fails. The
Java boolean expression is evulated in the same scope as the method
that it exists on for pre and post conditions and is executed in the
class scope for invariants. Asserts are evaulated in the scope that
they are placed. Post-conditions have a special keyword to represent
the return value of the method. This is $return. This
keyword is replaced by a special variable that is the return value
and matches the type of the return value allowing any method to be
called on it that would be called on the return value itself. Pre
and post conditions are allowed in the Javadoc comments for a method.
Invariants are allowed in the Javadoc comments for a class and
asserts may appear inside of Javadoc comments anywhere an executable
statement is allowed.
I wrote this program because I've used a program in the past called AssertMate and it really didn't implement assertions very well and had a lot of bugs. I talked with the people that wrote it and they decided to stop development, so I decided that being the programmer that I am, I'd write my own. Little did I know how much I was getting into, I've written compilers before, but this is a little more difficult, I actually have to modify someone else's code and it still needs to work the way they intended.
See one of the following pages for download links and usage instructions.
Last modified: Sun Dec 4 20:52:57 CST 2011