Java Q&A

Does Java support Design by Contract? Not directly, but as Krishnan shows here, support is still possible.


November 01, 1999
URL:http://www.drdobbs.com/jvm/java-qa/184411108

Nov99: Java Q&A

Krishnan is president of Man Machine Systems and can be contacted at mms@ giasmd01.vsnl.net.in or http://www.mmsindia.com/.


Design by Contract (DBC), pioneered by Bertrand Meyer (see Object- Oriented Software Construction, Second Edition, Prentice Hall, 1997), is widely acknowledged to be a powerful technique for writing reliable software. The three key elements of DBC are preconditions, postconditions, and class invariants. An example of a language that has direct support for DBC is Eiffel. Unfortunately, Java does not directly support DBC. However, there are third-party tools for Java that extend support to Design by Contract. One such tool is Reto Kramer's freely available iContract (http://www.reliable-systems.com/tools/). iContract parses Javasource code that is annotated with assertions inside Javadoc-style comments and generates modified Java source code where the assertion checking logic is appropriately embedded. The benefits of this approach are:

Two other equally interesting approaches for incorporating DBC in Java are Handshake (see "Adding Contracts to Java with Handshake," by Andrew Duncan and Urs Holzle, Technical Report TRCS98-32, Department of Computer Science, University of California, Santa Barbara, http://www.cs .ucsb.edu/TRs/ TRCS98-32.html) and jContractor (see "jContractor: A Reflective Java Library to Support Design by Contract," by Murat Karaorman, Urs Holzle, and John Bruno, Technical Report TRCS98-31, Department of Computer Science, University of California, Santa Barbara, http://www .cs.ucsb.edu/TRs/TRCS98-31.html). Handshake uses a separate contract file to dynamically synthesize a class file that incorporates assertions, whereas jContractor uses a design pattern approach. Each approach has strengths and limitations, and it is not my intention to discuss them. In this article, I'll present yet another approach, one that is part of a class-testing environment available from Man Machine Systems.

In a nutshell, our approach is this: We parse a Java source file suitably annotated with preconditions, postconditions, and invariants inside Javadoc comments and generate triggers in JMScript (a proprietary scripting language that is built on top of Java). These triggers are then executed by running the Java program (along with the triggers) by attaching the script interpreter to JVM via an extension DLL.

The first step is to add preconditions, postconditions, and invariants to Java code within Javadoc comments. Special tags are used for this; Table 1 lists these tags.

The assertions must conform to the syntax of JMScript Boolean expressions. To capture more complex conditions, you can use the special escape marker "@macro" to embed a JMScript code fragment. Table 2 shows how preconditions, postconditions, and invariants, are used in the context of a class.

We allow the contract to be specified for an interface, which gets propagated to its implementing classes. The same rule is applied to class hierarchies. For both interfaces and class hierarchies, preconditions are disjuncted, whereas postconditions and class invariants are conjuncted.

Consider Listing One, the canonical stack implementation in Java (to avoid confusion with JDK Stack class, I've named the example MyStack). Once a Java source file has been annotated as the one just mentioned, the next step is to use the preprocessor jmsassert utility to generate JMScript triggers for the assertions. In this case, we run jmsassert -s MyStack .java. The preprocessor creates the output files default_MyStack.jms and Startup.jms. The first file (Listing Two) contains JMScript triggers corresponding to the embedded assertions in Java source. The second file (Listing Three) makes it convenient to register the automatically generated triggers with JMScript at run time.

The third step is to compile the relevant Java source files. Assume that in addition to the MyStack definition as just mentioned, we also have the test driver class in Listing Four. This driver, along with the MyStack class, is compiled using a regular Java compiler such as "javac." The final step is, of course, to run the Java code with assertions enabled. To do this, invoke the Java interpreter using: java-Xdebug -Xnoagent -Djava.compiler= NONE -Xrunjmsdll:Startup StackTest. The CLASSPATH environment variable must be appropriately set to JDK1.2 run-time files, and additionally, must include mmsclasses.jar, which is supplied as part of the assertion environment.

The DLL jmsdll includes the JMScript interpreter. This DLL registers itself with JVM and assigns assertion triggers to the respective Java methods. When the JVM invokes a method, the call is intercepted by the DLL, and if a trigger (precondition, postcondition, or invariant) is associated with it, the corresponding JMScript trigger method is invoked. The trigger code in JMScript can access private elements of a class. This is a significant advantage in terms of testing. Though JMScript is primarily useful for bringing DBC to Java, it's designed for general-purpose scripting, and has some attractive features such as partial function specialization, multimethod, dynamic inheritance, and so on. Its strength derives from the underlying JVM. (For more details on JMScript, go to http://www.mmsindia.com/.)

One of the benefits of this approach is that the original Java source code is unmodified; what is tested with assertions is the same as what is executed normally. To run the test driver without enabling assertion code, simply run: java StackTest. The limitation that Java source must be available in order to specify contracts is overcome when you use JVerify (a tool that supports invasive testing by executing test drivers written in JMScript). That environment allows assignment of triggers to Java by inspecting compiled class files.

Conclusion

Although Java does not yet directly support Design by Contract, there are several ways to add such support. The approach I've presented uses a preprocessor to map contracts embedded in Java source code to triggers in the scripting language. Triggers are then automatically executed by an extension DLL that includes the JMScript interpreter. To run without assertions, all that is required is to run the Java program without the extension DLL. This approach ensures that the released program is identical to the one tested. To test a class, no modifications are necessary (other than source annotation).

DDJ

(Listings begin on page 116)

Listing One

/** 
     @inv (top >= 0 && top < max) 
*/
class MyStack {
        private Object[] elems;
        private int top, max;
    /**
        @pre (sz > 0)
        @post (max == sz && elems != null)
    */
    public MyStack(int sz) {
            max = sz;
            elems = new Object[sz];
    }
    /**
        @pre !isFull()
            @post (top == $prev (top) + 1) && elems[top-1] == obj
    */
    public void push(Object obj)  {
            elems[top++] = obj;
    }
    /**
        @pre !isEmpty()
            @post (top == $prev (top) - 1) && $ret == elems[top]
    */
    public Object pop()  {
            return elems[--top];
    }
    /**
        @post ($ret == (top == max))
    */
    public boolean isFull() {
            return top == max;
    }
    /**
        @post ($ret == (top == 0))
    */
    public boolean isEmpty() {
            return top == 0;
    }
} // End MyStack

Back to Article

Listing Two

/*  Trigger file for class #default.MyStack. Generated by JMSAssert on 
 * Monday, April 12, 1999. Any changes you make to this file will be 
 * overwritten if you regenerate this file.
 */
import macro;

// Postcondition for method - MyStack(int)
MyStackPost(meth, $obj, sz) {
    assertPost(($obj.max == sz && $obj.elems != null));
}
// Precondition for method - MyStack(int)
MyStackPre(meth, $obj, sz) {
    assertPre((sz > 0));
}
// Postcondition for method - void push(Object)
pushPost(meth, $obj, obj, $ret) {
    assertPost(($obj.top == 
              this.top$prev + 1) && $obj.elems[this.top$prev] == obj);
}
// Precondition for method - void push(Object)
pushPre(meth, $obj, obj) {
    this.top$prev = $obj.top;
    assertPre(!$obj.isFull());
}
// Postcondition for method - Object pop()
popPost(meth, $obj, $ret) {
    assertPost(($obj.top == this.top$prev - 1) && $ret == 
                                           $obj.elems[$obj.top]);
}
// Precondition for method - Object pop()
popPre(meth, $obj) {
    this.top$prev = $obj.top;
    assertPre(!$obj.isEmpty());
}
// Postcondition for method - boolean isFull()
isFullPost(meth, $obj, $ret) {
    assertPost(($ret == ($obj.top == $obj.max)));
}
// Postcondition for method - boolean isEmpty()
isEmptyPost(meth, $obj, $ret) {
    assertPost(($ret == ($obj.top == 0)));
}
MyStackinv(meth, $obj) {
    assertInv(($obj.top >= 0 && $obj.top <= $obj.max));
}
static {
    assertStrMyStack = {
        { "<init>(I)V", "POSTCONDITION", "MyStackPost" },
        { "<init>(I)V", "PRECONDITION", "MyStackPre" },
        { "push(Ljava/lang/Object;)V", "POSTCONDITION", "pushPost" },
        { "push(Ljava/lang/Object;)V", "PRECONDITION", "pushPre" },
        { "pop()Ljava/lang/Object;", "POSTCONDITION", "popPost" },
        { "pop()Ljava/lang/Object;", "PRECONDITION", "popPre" },
        { "isFull()Z", "POSTCONDITION", "isFullPost" },
        { "isEmpty()Z", "POSTCONDITION", "isEmptyPost" },
        { "", "INVARIANT", "MyStackinv" }
    };
    setClassTrigger("MyStack",     assertStrMyStack);
}
load() {}

Back to Article

Listing Three

//Startup trigger file - c:\ranga\jverify\Startup.jms
import macro;
load() {} 
static { 
   default_MyStack.load();
}

Back to Article

Listing Four

class StackTest {
    public static void main(String[] args) {
        MyStack s = new MyStack(2); // Can push at most two elements
            s.push(new Integer(1));
            s.push(new Integer(23));
            s.push(new Integer(0)); // Precondition violation here! 
    }
}

Back to Article


Copyright © 1999, Dr. Dobb's Journal
Nov99: Java Q&A

Table 1: Tags to specify DBC elements.


Copyright © 1999, Dr. Dobb's Journal
Nov99: Java Q&A

Table 2: JMScript Triggers Context.


Copyright © 1999, Dr. Dobb's Journal

Terms of Service | Privacy Statement | Copyright © 2024 UBM Tech, All rights reserved.