Adding Contracts to Java

Design by contract is a technique introduced by Meyer and implemented in Eiffel [Meyer]. It represents a way of specifying the requirements and deliverables between clients and suppliers of services in an OO system. A contract allows a method to specify what conditions need to be true before the method can function correctly, and in turn it specifies what will be true after it has executed. By ``publishing'' its contract, a method can then avoid often torturous validation code.

This promotes a programming style that is the opposite of the extremely defensive style seen in much systems programming. For example, instead of the C style of code such

 
if ((fp = fopen("file", "r")) == NULL) {
    fprintf(stderr, "cant open file\n");
    exit(1);
}
...

one might see (in informal notation)

require: "file" can be opened in mode "r"
fp = fopen("file", "r");
...

The runtime system is expected to check assertions, and if they fail then it will take appropriate action. This action may be to throw an exception (in languages that support exceptions) that may be caught by programmer code or left to the default runtime action.

Contracts may form documentation only or may be part of the runtime environment. Typical Eiffel systems allow this to be controlled by a compile-time switch, whereby code can be generated to enforce contract checking or to ignore it. Eiffel is unfortunately atypical among programming languages, in that it includes the option of runtime type checking. Most languages can only leave it to the documentation level, and even then, only in an informal manner.

Java has arisen as a major OO language, after a long gestation in private and a short period of visibility. Despite being developed over a period of years, when it was made public there were several unfinished features that were simply discarded. Amongst these, according to Gosling [Gosling], were assertions and a suitable contract mechanism. Now that Java is a standardised language with a formal mechanism for making changes, it may prove difficult or time consuming to incorporate these features into the language.

This paper discusses some of the possibilities that may be explored in adding contracts to Java, and reports on an experimental implementation using the ``reflection'' techniques available in Java. Reflection is a Java API that allows a program to examine classes and methods at runtime, and allows methods to be constructed and executed. It is shown that using the Reflection API is a feasible way of implementing contracts, but slow using current Java implementations. It also throws up several language design issues that cause difficulty in using the reflection technique, but which were probably unavoidable given the development environment and requirements.

It is not hard to devise syntax changes to Java with a corresponding semantic meaning. For example, a pop() method for a Stack could have its contract specified as

 
public Object pop()
              require(! empty())
              ensure(result == old getTOS() &&
                     getSize() == old getSize() - 1)
{
   ...
}

The semantics would be as in Eiffel - there is little need to rework this.

This would require changes to both the syntax and semantics of the Java language, and these are under the control of Sun as a standards organisation. For example, it would require introduction of keywords such as require, ensure and old, and a change in syntax to allow clauses to be specified for methods. This may occur in time, but if there is a desire to use contracts now, it may be too long to wait.

A mechanism that would work with no changes to language or involving any other techniques simply uses a style that each programmer conforms to. That is, each programmer includes the require clause on entry to a method, and calls the ensure code on exit.

Performing the require checking is easy. For example, the pop method would just make a call to the precondition code:

 
public Object pop() {
    if (empty())
        throw new RequireException();
    ...
}

Performing ensure checking is a little harder. Firstly, there is no single return point from a Java method. Fortunately, each method can have a finally section which is called as the method returns. Postcondition code can be placed in the finally section. Secondly, it is often necessary to refer back to values as they were on entry to the method. This can only be done by manual coding, saving the old values on entry to the method. Finally, the return value of a method may be needed in this checking. Whereas Eiffel returns values in the variable Result, there is no such variable in Java. This, or a variable playing a similar role, would need to be added as a convention.

This would lead to the pop method looking like

public Object pop() {
    // require
    if (empty())
        throw new RequireException();

    // capture values
    Object oldTOS = getTOS();
    int oldSize = getSize();
    Object result = null;

    try {
        // implementation
        result = s[--size];
        return result;
    } finally {
        // ensure
        if (! (result == oldTOS &&
            getSize() == oldSize - 1))
            throw new EnsureException();
    }
}

This has both advantages and disadvantages. The advantage is that it is an enforceable programming style that adds contract checking. Simple tools could be built to extract the contract from the code for documentation purposes.

The disadvantages are firstly that it is a little cumbersome, and coding standards may be observed in the breach unless rigorously maintained. Secondly, it is not possible to turn contract checking ``on'' and ``off' like it is with Eiffel at compile time. It is always on if present, off if absent.

A more serious problem is that it does not address inheritance. The semantics of contracts is that they are also inherited. The preconditions are or-ed together, and the postconditions are and-ed together. To perform this by hand in a large system with a lot of inheritance would be extremely difficult and time consuming.

A Java program exists in two static formats and is subject to a small number of operations. The two formats are source code and byte code as class files. The operations that can be performed include interpretation, transformation, compilation and reflection. (While other formats such as native code format are possible via native code compilers, they violate the ``write once, run anywhere'' paradigm and are not yet common except in transient form by some ``Just In Time'' compilers.) Contract checking may be introduced during any of the operations:

Interpretation

• The source code could be interpreted directly. An interpreter could introduce contract checking as part of method evaluation. No source level interpreters seem to be available as yet.
• The class files are usually interpreted on each platform. It would be possible to modify these interpreters but to do so would be at variance with the published Java Virtual Machine semantics.

Transformation

• Source code can be transformed into source code for the same language. Along the way can be added contract checking, even if the target language does not have such a feature. Kramer [Kramer] has developed such a transformation system, which is considered later.
• Class files can be transformed into other class files. This does not seem to have been explored yet.

Compilation

Compilation is a translation from source code to byte code. Eiffel compilers often have a switch to generate vanilla code or contract-checking code. No Java compilers do this as yet, probably due to a lack of the feature in the language.

Reflection

Reflection is a method whereby the runtime state of a program can be made available to the program, and conversely, the program can generate - at runtime - code to be executed at runtime. This has typically been used in two situations:

• a debugger allows execution steps to be mapped onto source code, and also allows runtime evaluation of expressions.
• Artificial Intelligence programs allow generation of code such as database queries from user input that can be dynamically interpreted.

A method of using reflection is considered in this paper, and contrasted against these other possibilities.

The iContract system by Kramer [Kramer] uses a preprocessor to generate Java code similar to that in section three which supplies contracts. The contract is given using extra comment keywords, similar in format to those used by the documentation tool JavaDoc:

/**
 * @pre !empty()
 * @post result == old getTOS() && \
         getSize() == old getSize() - 1)
*/
Object pop()
{ ... }

If the preprocessor is not run, contracts are not inserted into the code, and it runs like a standard Java program. If the preprocessor is run, it generates new Java code with the additional checks in place.

iContract is a fully functional mechanism to implement assertions, but it relies on a preprocessor external to any current Java compilation and runtime environment. It certainly provides a way of implementing contracts. Adding contracts using this system requires access to the source code of the classes. It cannot be added post-hoc to class files.

There is little else reported in the Java literature on assertions and contracts. The JDC Technical Tips column for February 1998 [JDCTips] carries a short article on an Assert class that can be used in programs. It does not address the full complexities of contracts, though.

Payne et al [Payne] discuss the problem of contracts in Java at some length. Their final proposal only covers the most basic of contract systems. It does not deal with ``old'' values, nor does it handle inheritance.

8.1 Contract class

Let us develop how this can be used to supply an interpretive layer to method calls. Instead of say, doing

Stack s = new Stack();
s.push(obj);

we want to write something like

Stack s = new Stack();
execute(s.push(obj));

Now execute() will not be a method of any of the application classes: it may need to be called for any method of any class. So we need a class, called say Contract with a static method execute(). This is the only public method needed for this class. It may throw exceptions, say a RequireException and an EnsureException.

The parameters to execute() are a little messy. We cannot simply write s.push(obj) because this will simply evaluate the method before we get a chance to interpret it. We need to pass the object as one parameter and the name of the method as another. This will allow the introspection/reflection mechanism to find the method and execute it. The parameters to the method call, on the other hand, must be evaluated at the time of the call. We need a list of method parameters, evaluated immediately. The execute() method will then have three parameters: the object with the method, the method as a string, and an array of evaluated parameters of the method. The call will look like

Object parameters[] = new Object [] {obj};
Contract.execute(s, "push", parameters);

This constructs a parameter array with one element, obj, and then calls the method execute() with the object, the string name of the method and the parameter array. This syntax is not appealing, but unavoidable using this mechanism.