Deprecated: Function set_magic_quotes_runtime() is deprecated in /home/raedan/public_html/textpattern/lib/txplib_db.php on line 14
State of Flow: InvariantJ::projects

InvariantJ

InvariantJ is a mechanism for implementing class invariant checking in Java. It uses a simple method naming convention to allow developers to create as many invariants as they wish. If one or more invariants fail at runtime, an exception will be thrown with a message containing the full list of violated invariants.

What are Class Invariants?

Class invariants are a major part of the Design by Contract technique. For a good discussion of this, see Bertrand Meyer’s Object Oriented Software Construction. Whether or not Design by Contract is applied, specifying invariants of classes in any system is useful in at least three ways:

Simply put, a class invariant is something that must be true about any instance of the class when that instance is in a quiescent state. If an object is quiescent and one of its invariants is violated, it usually means that there is a coding error in the class or in its hierarchy.

Objects are quiescent when none of their behaviours are in the process of executing. If a behaviour is executing, an invariant may be temporarily violated, to be restored subsequently before a quiescent state is reached again.

This is analagous to integrity constraints in an RDBMS which must hold on both sides of a transaction but are not required to hold during the transaction.

How is this Different from Pre-Conditions and Post-Conditions

A class invariant is a kind of pre- and post-condition. However, pre- and post-conditions apply to single behaviours only and typically verify that parameters are appropriate, that the object’s state is suitable for the execution of the particular behaviour or that the results of execution are as expected. A class invariant specifies both pre- and post conditions for all relevant behaviours but is only tested just before an object leaves a quiescent state and just after it returns to one.

Implementing Class Invariants

InvariantJ allows any class to easily specify invariants. All that is required is the addition of one or more methods that conform to a naming convention and a signature. An invariant checking method must:

Invariant checking methods can have any visibility. However, visibility of at least protected is recommended since it allows subclasses to override the invariant.

At the entry and / or exit of appropriate behaviours, all invariant methods are invoked. After all invariants have been checked, if any violations have occurred, a com.stateofflow.invariantj.InvariantViolationError is thrown with a message containing information about all invariant violations.

Examples can be found in the documents provided with the distribution.

Compiling / Instrumenting

In order to use InvariantJ, you must have an Ant build file. During the build of you project, InvariantJ will decorate the byte code of your compiled classes using Javassist

The documents provided with the distribution have examples of instrumenting code with InvariantJ.

Using InvariantJ with IDEs

InvariantJ can be used within popular IDE’s that have a reasonable level of Ant integration. Instructions for doing this are included in the distribution.

Where Precisely are Invariants Checked

For the purposes of this discussion, constructors should not be considered as method — the general term ‘behaviour’ denotes both methods and constructors.

Static Model

The following points specify the static model for invariant checking. Whether invariants are actually checked at each of these points is subject to gating by the Dynamic Model specified below:

Dynamic Model

InvariantJ has a dynamic aspect to its behaviour that means that for every thread of execution, an object’s class invariants will only be verified at the highest point in the stack that the flow of execution encountered the object and only if the behaviour concerned is public.

The reason for this is that sending a message to this can reasonably be considered an implementation detail, whether or not the behaviour that intercepts that message is public. The same message originating outside the target object will result in an invariant check however, pursuant to the object not having been the recipient of any messages higher in the stack.

The argument is a little more tenuous for disabling invariant checking of an object when, for example, the object sends a message to another which sends a message (intercepted by a public method) back to the first. In this case, InvariantJ considers that the two objects are collaborating in some shared work and requires only that the invariants are maintained for each object upon initial entry and final exit.

It is certainly possible to work with a model of class invariants that is specified entirely by InvariantJ’s Static Model regardless of the dynamic context — in fact, it would have been far easier to implement InvariantJ this way. However, it is felt that the implementation provided allows the powerful notion of class invariants to be applied without requiring hoops to be jumped through, although it is acknowledged that this implementation does potentially lose some ‘locality’ should a violation occur.

The single exception to the ‘first encounter’ rule is that when constructors are chained, the testing of invariants will occur on exit of every public constructor in the chain. This is due to the requirement expressed in section 8.8.7 of the Java Language Specification that a constructor must begin with an invocation of a superclass’s constructor or another constructor declared in the class. It is therefore not possible for InvariantJ to decorate the bytecode in such a way that it can note that one constructor has been invoked by another. This only has consequences if the chain is between two constructors of the same class (as opposed to chaining a constructor to a superclass constructor), in which case it may be necessary to break the chain and extract the body of the invoked constructor into a non-public behaviour that both constructors in the original chain can use.

Software Versions