Need help with cofoja?
Click the “chat” button below for chat support from the developer who created it, or find similar developers for support.

About the developer

140 Stars 17 Forks GNU Lesser General Public License v3.0 116 Commits 15 Opened issues


Contracts for Java

Services available


Need anything else?

Contributors list

# 588,476
25 commits
# 7,815
2 commits
# 155,876
2 commits


Contracts for Java, or Cofoja for short, is a contract programming framework and test tool for Java, which uses annotation processing and bytecode instrumentation to provide run-time checking. (In particular, this is not a static analysis tool.)

I originally wrote Cofoja when interning at Google in 2010, based on prior work on Modern Jass. It was open-sourced in early 2011, and has since been maintained by myself, with the help of a small community.



You can get official Cofoja builds from the Central Repository, group ID:

, artefact ID:

Pre-built JAR files are available on the GitHub release page:

Each release comes in four flavours.

is the basic version, which contains every feature Cofoja has to offer.
builds are bundled with a compatible version of the ASM library.
are debug builds that include self-check contracts on the annotation processor and library themselves.

If you are confused about which version to choose, pick either the plain

JAR file if you already have the ASM library installed, or plan to install it by other means, or the
JAR file if you want a single JAR file that works out of the box.

The class files are compiled for Java 6. Cofoja itself depends on features not available to older versions of Java.



Building Cofoja requires:

  • JDK 6 or higher, for annotation processing and bytecode instrumentation.
  • ASM 5.x (or higher versions with ASM5-compatible API), for bytecode instrumentation.
  • JUnit 3.8 or 4.x if you want to run tests.
  • Ant 1.9.1 or higher for the build script.

If Ivy is installed, calling the

Ant target retrieves the dependencies automatically.

Alternatively, put JAR files from dependencies under the

folder, in the current directory. The directory does not exist by default and must be created.

In order to enable contract checking at run time, Cofoja binaries and dependencies are needed. Normal execution (with contracts disabled) does not require Cofoja or any of its dependencies.


The build script reads properties from the user-provided
file. See
for a list of configuration options to adjust to fit your build environment. Most importantly, you may want to adjust the path to the
on Mac OS) file, which should be provided by the JDK.

Ant targets

The default target,

, builds all four release JAR files. To include only those without self-contracts, execute the

By default, the produced JAR files are placed in the

folder, in the current directory.

You should run the

target to check that your build of Cofoja behaves (somewhat) as expected.


Cofoja supports a contract model similar to that of Eiffel, with added support for a few Java-specific things, such as exceptions.

Some general understanding of contract programming (also called design by contract) is required to use Cofoja effectively. If you have no idea what this is, Wikipedia may be a good place to start:


In Cofoja, contracts are written as Java code within quoted strings, embedded in annotations. E.g.,

@Requires("x < 100")
states that
must be less than 100. Any Java expression, except anonymous classes, may be used, provided the string is properly escaped.

An annotation binds a contract to a code element: either a method or a type. Cofoja defines three main annotation types, which live in the
  • @Requires
    for method preconditions;
  • @Ensures
    for method postconditions;
  • @Invariant
    for class and interface invariants;

Contract annotations work on both classes and interfaces. For convenience, arrays of quoted expressions are accepted, and behave as if the components were separated by

. E.g.,
@Ensures({ "x > 0",
"x < 50" })
is equivalent to
@Ensures("x > 0 && x < 50")

Method contracts

A method may have preconditions and postconditions attached to it. Together, they specify the contract between caller and callee: if the precondition is satisfied on entry of the method, then the caller may assume the postcondition on exit. The precondition is what the callee demands of the caller, and in return the caller expects the postcondition to hold after the call.

As an example, consider the following specification of the square root function, which states that for any non-negative double

will return a non-negative result.
@Requires("x >= 0")
@Ensures("result >= 0")
static double sqrt(double x);

As shown in this example, a precondition may access parameter values; in fact, preconditions and postconditions are evaluated in the context of the method they are bound to. More precisely, each annotation behaves as if it were a method, with the same arguments and in the same scope as the qualified method. In terms of scoping, the previous code is equivalent to the following:

static void sqrt_Requires(double x) {
  assert x >= 0;
static void sqrt_Ensures(double result) {
  assert result >= 0;
static double sqrt(double x);

In addition, postconditions may contain a few extensions:

  • As we have seen, they may refer to the returned value, using the
  • Within a postcondition,
    is a keyword which is followed by a single parenthesized expression, such that
    old (x)
    evaluates to the value of
    on entry of the method invocation.
  • An
    expression is evaluated in the same context as preconditions and has access to the same things, including parameter values.

Given this, a more complete specification of

might be:
@Requires("x >= 0")
@Ensures({ "result >= 0", "Math.abs(x - result * result) < EPS" })
static double sqrt(double x);

At run time, when contracts are enabled, preconditions and postconditions translate to checks on entry and exit, respectively, of the method. A failure results in a

being thrown, depending on the origin: failure to meet a precondition means that the method was called incorrectly, whereas an unsatisfied postcondition points to a bug in the implementation of the method itself.

Class and interface contracts

A class or interface may have associated invariants. Instead of specifying a contract between a caller and a callee, those invariants describe the state of a valid object of the qualified type. Calling methods on an object may cause it to change; invariants guarantee that after any such change, the object remains in a consistent state.

Of course, internal operations are allowed to muck around and temporarily invalidate invariants to do their job, but they agree to eventually put everything back into their proper places. Intuitively, any operation made against

is considered internal and does not need to obey the invariants. Only method invocations on other variables do.

In Cofoja, when contracts are enabled, invariants are checked on entry and exit of method calls on objects not already in the call stack (including

). Failure results in an
exception and indicates that the guilty method has left the object in an inconsistent state.


Contracts apply to all objects of the associated type, including any instances of derived classes: all implementations of a contracted interface must honor the interface contracts, all children of a class must honor the contracts of their parent.

In addition, derived types may refine those contracts by adding their own preconditions, postconditions and invariants to the mix. However, they cannot replace the inherited contracts, only augment them according to the following subtyping rules.

Preconditions may be weakened, i.e., methods may be overriden with implementations that accept a wider range of inputs. Callers that access the object through a superclass or interface need only establish the parent contracts. In Cofoja, a method checks that either its inherited or its own preconditions are satisfied.

Postconditions may be strengthened, i.e., methods may be overriden with implementations that produce a smaller range of outputs. Callers that access the object through a superclass or interface expect at least the parent contracts. In Cofoja, a method checks both its inherited and its own postconditions.

Invariants may be strengthened, i.e., classes and interfaces may be derived to restrict the set of valid states. An object must qualify as a consistent value of any of its superclasses or interfaces. In Cofoja, a type asserts both its inherited and its own invariants.

Other features

Import annotations

Previously, we have used

in our examples, which resides in
, and is thus available to any Java code. For other symbols, we may need to import a class or package. Imports for contracts are kept separately from those of the main file. The
annotation specifies names to be imported for use in contract code within the associated type. It must be put on the enclosing type and accepts an array of strings, each one containing an import pattern, compatible with the
Java statement.

Java expressions

Contracts are made of Java expressions, with the addition of several keywords. Cofoja uses the Java compiler from the standard tools package and hence supports the same language as provided by that compiler (which should usually be the same as that of the top-level compiler).

However, some expressions may generate bridges or other synthetic methods in addition to their direct translations to bytecode. Such artifacts need to be identified and handled specially by Cofoja. The following features are currently known to require particular processing:


Supported Description
Inner class accesses Yes May generate

Anonymous classes No Generate additional class files
Java 8 lambda expressions Yes Generate

Since uses of synthetic methods follow no set rules, compilers other than Javac may opt for different compilation strategies. At the moment, no such incompatible scheme has been reported.


With respect to Cofoja, constructors behave slightly differently from other methods. They assert invariants, but only on exit, and may be attached to preconditions and postconditions. However, a very important distinction is that constructor preconditions are checked after any call to a parent constructor. This is due to

calls being necessarily the first instruction of any constructor call, making it impossible to insert precondition checks before them. (This is considered a known bug.)

Exception handling

When an exception is thrown from within a contracted method, normal postconditions are not checked by Cofoja, as they may refer to a result that does not exist.

Instead, the

annotation is provided. It functions similarly to
but accepts an alternating list of exception type names to catch and matching postcondition expressions, as quoted strings. Within those exceptional postconditions, the keyword
refers to the exception object that has been thrown.

A possible use of

is to guarantee that exceptional method exits do not inadvertently alter the state of the object.
class RestrictedInteger {
  int x;

@Ensures("x == y") @ThrowEnsures({ "IllegalArgumentException", "x == old (x)" }) void setX(int y) throws IllegalArgumentException { ... } }


Contracts for Java consists of an annotation processor, an instrumentation agent, as well as an offline bytecode rewriter. The annotation processor compiles annotations into separate contract class files. The instrumentation agent weaves these contract files with the real classes before they are loaded into the JVM. Alternatively, the offline bytecode rewriter can be used to produce pre-weaved class files that can be directly deployed without requiring the Java agent or ASM library at run time.

The pre-built JAR files contain both the Java agent and annotation processor. The latter is named

(in the
package); the agent can be loaded directly by specifying the JAR file (e.g., as an argument to the

To execute code compiled with contract checking enabled, make sure the generated files (additional

files) are in your class path and enable the Cofoja JAR file as a Java agent.

Or use the offline instrumenter, which lives in the

class, under the
package, and takes paths to class files as command-line arguments.

Run-time contract configuration

Selective contracts

When using the Java agent, contract evaluation can be enabled selectively, similar to how assertions can be toggled on and off for specific types. Whether contracts are checked on methods of a given type is determined at load time and may not be changed afterwards.

These settings are controlled through a user-defined configurator object. As part of its early start-up procedure, the Java agent attempts to create an instance of the configurator class, whose name is provided through the
JVM property. It then calls the
method on the newly created object, passing it an argument of type
(from package


object provides methods such as
, to enable or disable contracts selectively. Each method accepts an import-like string pattern. In case of pattern overlap, the behavior specified by the last matching call is retained.

Disabling contracts for a specific type does not prevent its contracts from being inherited and checked correctly for the derived types.


The blacklist is controlled through the

, which also take patterns, similarly to the contract selection methods.

Ignoring a pattern is different from disabling contracts for that pattern. A blacklisted type is not be examined at all by the Java agent; in particular, it is not searched for contracts and its bytecode is not modified in any way. It is assumed to contain no contracts; thus, derived types inherit nothing from it.

Debug tracing

For debug purposes, Cofoja may be instructed to print a trace to stderr of contract that are evaluated. Compilation support for tracing is provided by the
annotation processor flag. The actual trace is obtained by running the contracted program with the
JVM property set to

Quick reference


All annotations reside in the


Checked on Inheritance

| Object entry and exit | And
| Entry | Or
| Normal exit | And
| Abnormal exit | And



May appear in Description

| Value on method entry
| Value to be returned
| Exception thrown

Annotation processor options

All option names reside in the
name space. Options that have a Javac counterpart are passed down to the underlying Java compiler used to compile contract code. In most cases, they should match those used to compile the main project.


Type Javac option Description

| path |
| Class path for contract code
| path |
| Where to find source files
| directory |
| Where to put compiled contract files
| flag | | Enable run-time logging support
| directory | | Where to put generated source files

Additionally, you may want to pass

(or equivalent) to the Java compiler, so it only runs the annotation processor, which will generate compiled contract files without producing the normal class files. This is recommended for medium-to-large projects.

Java agent properties

All properties reside in the
name space.


Type Description

| String | Configurator class name
| String | Where to dump instrumented class files
| Boolean | Print a trace of evaluated contracts to stderr

requires contracts compiled with the
annotation processor option.

Run-time contract configuration methods

All methods live in



| Check preconditions for all methods of class
| Do not check preconditions for any method of class
| Check postconditions for all methods of class
| Do not check postconditions for any method of class
| Check invariants for class
| Do not check invariants for class
| Do not search class for contracts
| Search class for contracts


Contracts for Java is a not-so-young project. Please help make it better by reporting bugs at:

For general questions and help with using Cofoja, you can reach out to the dedicated Google discussion group:

We use cookies. If you continue to browse the site, you agree to the use of cookies. For more information on our use of cookies please see our Privacy Policy.