Dr. Dobb's is part of the Informa Tech Division of Informa PLC

This site is operated by a business or businesses owned by Informa PLC and all copyright resides with them. Informa PLC's registered office is 5 Howick Place, London SW1P 1WG. Registered in England and Wales. Number 8860726.

Channels ▼

JVM Languages

Java Q&A

Nov99: Java Q&A

Krishnan is president of Man Machine Systems and can be contacted at [email protected] 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:

  • Because assertions are embedded inside comments, they are transparent to the Java compiler.
  • No costly source modifications are needed to regenerate assertion-disabled byte code; simply recompiling the original source with a normal Java compiler is all that is needed.

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.

  • Class Invariant (@inv) should be defined inside a Javadoc comment before the class definition. The marker is followed by a Boolean expression that may reference any element of the class or its direct/indirect bases, including private elements.
  • Precondition (@pre) must be defined within Javadoc comments preceding the respective methods. The marker is followed by a Boolean expression, as in the class invariant. Also, the condition may reference arguments passed to the method.

  • Postcondition (@post) is specified within Javadoc comments preceding the respective methods. The condition may be any Boolean expression, as in the precondition case. The Boolean expression may also use the qualifier $prev on an expression to denote the expression's value at the method's entry point. For example, $prev (top) denotes the value of variable top at method entry (without the qualifier, it indicates its current value). The keyword $ret may appear in the condition to denote the method's return value.

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.


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).


(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;
// Postcondition for method - Object pop()
popPost(meth, $obj, $ret) {
    assertPost(($obj.top == this.top$prev - 1) && $ret == 
// Precondition for method - Object pop()
popPre(meth, $obj) {
    this.top$prev = $obj.top;
// 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 { 

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

Related Reading

More Insights

Currently we allow the following HTML tags in comments:

Single tags

These tags can be used alone and don't need an ending tag.

<br> Defines a single line break

<hr> Defines a horizontal line

Matching tags

These require an ending tag - e.g. <i>italic text</i>

<a> Defines an anchor

<b> Defines bold text

<big> Defines big text

<blockquote> Defines a long quotation

<caption> Defines a table caption

<cite> Defines a citation

<code> Defines computer code text

<em> Defines emphasized text

<fieldset> Defines a border around elements in a form

<h1> This is heading 1

<h2> This is heading 2

<h3> This is heading 3

<h4> This is heading 4

<h5> This is heading 5

<h6> This is heading 6

<i> Defines italic text

<p> Defines a paragraph

<pre> Defines preformatted text

<q> Defines a short quotation

<samp> Defines sample computer code text

<small> Defines small text

<span> Defines a section in a document

<s> Defines strikethrough text

<strike> Defines strikethrough text

<strong> Defines strong text

<sub> Defines subscripted text

<sup> Defines superscripted text

<u> Defines underlined text

Dr. Dobb's encourages readers to engage in spirited, healthy debate, including taking us to task. However, Dr. Dobb's moderates all comments posted to our site, and reserves the right to modify or remove any content that it determines to be derogatory, offensive, inflammatory, vulgar, irrelevant/off-topic, racist or obvious marketing or spam. Dr. Dobb's further reserves the right to disable the profile of any commenter participating in said activities.

Disqus Tips To upload an avatar photo, first complete your Disqus profile. | View the list of supported HTML tags you can use to style comments. | Please read our commenting policy.