Implement Design by Contract for Java using dynamic proxies

Write bug-free code with the DBCProxy framework

While developing software and its subsequent versions, developers often enhance functionality by modifying existing code. However, developers who modify or enhance that code are usually not its original authors. Depending on the complexity of code and its supporting documentation, and the clarity of requirements, enhancements may present a difficult problem.

For instance, suppose you could enhance an existing application by performing the following tasks: extend a class and override a method in the extended class. Questions arising during the design and implementation phase would most likely include: Should the super class method be called? If the super class method is called, should the overriding method call the super class method at the beginning or end of the overriding method?

Many developers experience this situation everyday as they maintain and enhance existing software. As a result, they are at the mercy of requirements specifications and existing software documentation to understand software's complexity. If either artifact is too vague, the developer may find designing and implementing the necessary changes difficult.

However, software that includes assertions, based on the Design by Contract (DBC) theory, combats that problem. You could clearly design and subsequently enhance that software because those assertions would advertise class, method, and interface contractual obligations. The assertions would provide a clear enforceable picture of the existing software's state, behavior, and interface. Thus, they make enhancing existing software much easier for developers.

In this article, I present a DBC for Java framework called DBCProxy. This framework uses dynamic proxy classes, which were introduced in Sun Microsystems's JDK 1.3. I'll begin by briefly introducing DBC, and then I'll describe DBCProxy's architecture and how you can use it in your development process.

Introducing DBC

When software developers perform object-oriented analysis and design (OOAD), they strive to identify appropriate abstractions within a problem domain. Additionally, they label these abstractions with a specific name and usually provide some additional text to further clarify it. In the software construction and implementation phase, developers utilize Java to transform these abstractions into Java interfaces, classes, and methods. These constructs let you advertise an abstraction's purpose and functionality.

Descriptive text and identifying names may offer a great deal of information about an abstraction. However, rarely do they provide a precise specification. Descriptive text may contain enough information to make it sound like a detailed specification, but plain text is often ambiguous and not enforceable.

DBC provides a formal way of writing detailed specifications with assertions; these can be viewed as enforceable contracts between the designer/developer of a class or interface (abstraction) and the class or interface client. To accomplish this, DBC uses three assertion types:

  • Preconditions: An object's valid state and the arguments passed to a method prior to a method call
  • Postconditions: An object's valid state and the arguments passed to a method after a method call
  • Class invariants: An object's valid state

When looking at contractual responsibilities, the client must satisfy the precondition prior to invoking a method. The supplier must satisfy the postcondition and class invariant. This clarifies the functionality provided and establishes an enforceable contract between a client and a supplier. Consequently, when a contract breaks (a software bug exists), you can easily tell whether the client or supplier did not satisfy its assertion(s). Also important to understand, DBC assertions are not part of the implementation. Rather, they are part of a class or interface specification. DBC clearly separates specification (what) from implementation (how). You can find additional information on DBC in Resources.

DBC in the development process

As software grows larger and more complex, the need to identify architectures and designs that satisfy such requirements as scalability, availability, security, and so on proves more important to the software's overall success. On large software projects, a team of software architects and software designers commonly specify an API for a subsystem and subsequently hand it off to a developer team to implement. The API specification is often ambiguous; in some cases, the architect or designer may interpret the specification differently than the implementer, which may introduce defects. Since DBC is assertions-based, it can help in these situations. Additionally, DBC possesses the following advantages:

  • Assertions communicate specifications clearly and precisely.
  • Class methods and interfaces are specified with assertions so architecture and design require more thought.
  • When the implementation doesn't satisfy assertions, assertion exceptions are thrown during software testing.
  • API users can begin implementation since DBC-based specifications clearly and precisely communicate what the client must do in a precondition. In addition, the API specification communicates the API functionality in the form of a postcondition and invariants.

DBC applied to Java

As described above, DBC and assertions are not part of the implementation. Rather, they are part of a class or interface specification. How can we isolate DBC and assertions from the implementation in Java? Here's an example of how we might apply assertions in Java: Suppose method m(x) asserts that x is never null. In Java, the code may form:

void m(Object x)
{
  assert(x != null);
}

In the above example, the assertion is part of the implementation; instead it should be part of the specification. In other words, the above example should form:

assert(x != null)
void m(Object x)
{
}

or

void m(Object x)
assert(x != null)
{
}

However, neither form will compile in Java. To effectively utilize DBC in Java, we must find an alternative mechanism, possibly Java's /** */ comment syntax. The special comments /** */ are most commonly used in front of class and method declarations. If you placed assertions inside these special comments, the Java compiler javac would ignore them.

You could also add assertions in Java by using tags. The documentation tool javadoc supports a variety of predefined tags. However, you can define additional tags that javadoc and its Doclet architecture can process.

In this article, I introduce three new tags to support assertions and DBC in Java. One for each assertion type:

  • @pre for preconditions
  • @post for postconditions
  • @invariant for invariants

The rules for these new tags are as follows:

  • You must follow all tags with a

    logical_statement

    , except when you use keywords

    $implies

    and

    $return

    (described later):

     @pre logical_statement [, wait]
    @post logical_statement
    @invariant logical_statement
    
  • The logical_statement uses regular Java syntax. You use the text inside the logical_statement as-is (again, except when using $implies and $return); in other words, it is not further parsed. Not supporting a separate DBC syntax was a clear design goal of the DBCProxy framework.
  • You must prefix method calls on a primary object with obj(). A primary object is the object for which the assertion is being made. For example, if a primary object's interface has a method called count(), then @pre obj().count() >= 0 is a valid precondition. To make this a valid postcondition or invariant, simply replace @pre with @post or @invariant.
  • To apply an assertion conditionally, you use the keyword $implies, which has the following syntax:
    @pre logical_statement $implies logical_statement
    @post logical_statement $implies logical_statement
    @invariant logical_statement $implies logical_statement
    

In the following sections, I'll present rules and examples for the three assertion types, @pre, @post, and @invariant, in more detail.

Preconditions

You declare preconditions in a method's special comments section, as described above. Preconditions can assert arguments and call methods on the primary object. In the following example, the precondition asserts the object x passed to the put() method must not equal null:

/**
* @pre x != null
*/
public void put(Object x);

The next example asserts the primary object must not be empty and calls the method empty() on the primary object as part of the precondition declaration:

/**
* @pre !obj().empty()
*/
public Object item(Object x);

I describe the wait keyword, which optionally follows the logical_statement, in the section "Separate Objects."

Postconditions

You also declare postconditions in the method's special comments section. A postcondition has the same capabilities as a precondition but possesses two additional features:

  • It has access to the primary object's state before the method call by prefixing that call with

    old()

    . This example uses

    old()

    and asserts the method

    count()

    will increment by one, as a result of executing the

    put()

    method:

    /**
    * @post obj().count() == old().count() + 1
    */
    public void put(Object x);
    
  • If a method has a return value, you use the keyword $return. This example uses $return and asserts the item() method will never return null:
    /**
    * @post $return != null
    */
    public Object item();
    

Invariants

You declare invariants in the class/interface special comments. Invariants can only call methods on the primary object. This example asserts the method count() will always return a value greater than or equal to zero:

/**
* @invariant obj().count() >= 0
*/
public interface Stack
{
  public int count();
}

To better illustrate how to use preconditions, postconditions, and invariants, Listing 1 shows a Stack interface with those assertion types. This example also illustrates how a familiar interface may appear when you use DBCProxy:

Listing 1. Stack interface

1 package dbc.test;
2 /**
3 * LIFO Container
4 * @invariant obj().count() >= 0
5 * @invariant obj().count() < obj().capacity()
6 * @invariant obj().empty() == (obj().count() == 0)
7 * @invariant obj().full() $implies !obj().empty()
8 */
9 public interface Stack
10{
11 /**
12 * Maximum number of stack elements
13 */
14 public int capacity();
15
16 /**
17 * Number of stack elements
18 */
19 public int count();
20
21 /**
22 * Top element
23 * @pre !obj().empty(), wait
24 */
25 public Object item();
26 /**
27 * Is stack empty?
28 * @post $return == (obj().count() == 0)
29 */
30 public boolean empty();
31
32
33 /**
34 * Is stack full?
35 * @post $return == (obj().count() == obj().capacity())
36 */
37 public boolean full();
38
39 /**
40 * Add obj on top
41 * @pre !obj().full(), wait
42 * @post !obj().empty()
43 * @post obj().item() == obj
44 * @post obj().count() == old().count() + 1
45 */
46 public void put(Object obj);
47
48 /**
49 * Remove top element
50 * @pre !obj().empty()
51 * @post obj().count() == old().count() - 1
52 */
53 public void remove();
54
55 }

In Listing 1, lines 4 through 7 declare invariants; line 23 declares a precondition on method item(); and line 28 declares a postcondition for method empty(). At lines 41 through 44, method put(Object) has one precondition and three postconditions.

You can consider this example a detailed specification of the Stack interface. Now that you've seen an interface with assertions defined, you can generate assertion files for Stack. However, before doing so, I will present the DBCProxy framework in more detail.

The DBCProxy framework

Figure 1 shows the most important classes in the DBCProxy framework.

Figure 1. DBCProxy's important classes

You only need to interact with two DBCProxy classes for this example:

  • dbc.DBC: Represents the DBCProxy runtime. It has two static methods that can turn a regular object into a DBC-enabled object.
  • dbc.generator.DBCGenerator: Generates DBC assertion files used by the DBC runtime.

Generate Java assertion files

You need to ensure that assertion tags declared in the Stack interface turn into Java source files so the JVM can execute them.

The dbc.generator.DBCGenerator class above translates assertion tags into Java code. This class is implemented as a doclet; therefore, it can use the javadoc utility to do all the parsing and use the assertion tags @pre, @post, and @invariant.

To use DBCGenerator for tag translation, type the following at the command prompt:

java -classpath [%JAVA_HOME%/jdk1.3/lib/tools.jar;classpath of
dbcproxy.jar] dbc.generator.DBCGenerator -sourcepath src 
-d src dbc.test.Stack

The source file is located in the -sourcepath directory, and the resulting file generates in the -d (destination) directory. When DBCGenerator executes, it generates three files that will be located in the directory src/dbc/test/__assertions. These files are:

  • PreStack.java: Contains preconditions for Stack.java
  • PostStack.java: Contains postconditions for Stack.java
  • InvariantStack.java: Contains an invariant for Stack.java

Figure 2 illustrates how the generated assertion files relate to the framework.

Figure 2. Generated assertion files

You then compile these generated files into Java class files using a Java compiler.

DBC property file

Before you can validate the Stack using DBC, you must enable the DBC runtime environment by creating a property file called dbc.properties. That property file has three property names:

  • dbc.precondition
  • dbc.postcondition
  • dbc.invariant

You enable the DBC runtime environment at the package level. In the Stack example, we enable DBC for all assertion types using the following settings in the dbc.properties file:

dbc.precondition=dbc.test
dbc.postcondition=dbc.test
dbc.invariant=dbc.test

Test the DBC-enabled stack

To create a Stack instance and validate the assertions defined, you need to implement the Stack interface.

Listing 2 shows Java class StackImpl, which implements the Stack interface. Notice that the package is declared as dbc.test, which is the package identified in the dbc.properties file described in the previous section:

Listing 2. StackImpl class

1 package dbc.test;
2
3 import java.util.*;
4
5 public class StackImpl implements Stack 
6 {
7 public StackImpl(int capacity)
8 {
9 this.capacity = capacity;
10 vector = new Vector(capacity);
11 }
12
13 public int capacity()
14 {
15 return capacity;
16 }
17
18 public int count()
19 {
20 return vector.size();
21 }
22
23 public Object item()
24 {
25 return vector.elementAt(vector.size() - 1);
26 }
27
28 public boolean empty()
29 {
30 return count() == 0;
31 }
32
33
34 public boolean full()
35 {
36 return count() == capacity();
37 }
38
39 public void put(Object obj)
40 {
41 vector.addElement(obj);
42 }
43
44 public void remove()
45 {
46 vector.removeElementAt(vector.size() - 1);
47 }
48
49 private int capacity;
50 private Vector vector;
51}

With this Stack implementation, we create a DBC-enabled Stack instance. (StackImpl could include assertions, so assertion files could require generation for those assertions as well.)

To create that DBC-enabled instance, you use the dbc.DBC class from Figure 1. As stated earlier, this class represents DBCProxy's runtime environment. dbc.DBC has a public method with the following signature:

public static Object newInstance(Object obj) throws Throwable

The newInstance() method is almost the complete DBCProxy API. The argument passed to newInstance() is the primary object (in this case, StackImpl). You can safely cast the returned object to the Stack interface because StackImpl implements the interface; newInstance actually returns a dynamic proxy that implements all interfaces that StackImpl implements.

The following code shows how to create a DBC-enabled StackImpl instance:

Stack stack = (Stack)DBC.newInstance(new StackImpl(10));

That's it. In the code above, stack is a Stack instance that enforces the preconditions, postconditions, and invariant defined by the assertion tags. Figure 3 shows a simplified version of what happens when you instantiate the DBC-enabled stack.

Figure 3. Instantiate the DBC-enabled stack. Click on thumbnail to view full-size image.

Figure 3 illustrates the following sequence of steps:

  1. The primary object StackImpl instantiates
  2. The primary object passes to method DBC.newInstance(), which instantiates DBC (the invocation handler)
  3. Using naming conventions and reflection, the invocation handler DBC finds, instantiates, and stores all StackImpl's assertion classes in the DBC instance
  4. DBC checks the invariants
  5. A dynamic proxy object, with the DBC instance as its invocation handler, instantiates and returns to the client

Note: StackImpl does not specify any new assertions. However, StackImpl does inherit the assertions defined in Stack and as a result must adhere to them. Figure 3 (and later Figure 4) illustrates the inheritance nature of the defined assertions.

Now that a DBC-enabled Stack instance exists, we can test its contractual obligations. For example, to see what happens when a Stack client violates a precondition assertion, let's call method stack.item() before any object is put on Stack. Here is the client code:

Object obj = stack.item();

Clearly the above statement violates the precondition at line 23 in Listing 1. Line 23 implies that an item from stack cannot be retrieved if the stack is empty. Therefore the following error message displays when the code executes:

Precondition violated: !obj().empty() at dbc.test.StackImpl.item

Clearly, the client caused this violation; it should have known not to retrieve an item from an empty stack.

Postconditions can also be violated. Remember these are the supplier's responsibility; in this example, StackImpl is the supplier. Therefore, to violate a postcondition, you must change the StackImpl implementation by removing or commenting out the put() implementation at line 41 in Listing 2. Then, if a client executes the following code segment that uses put():

stack.put("Any Object");

then StackImpl will violate at least two postconditions declared at lines 43 and 44 in Listing 1. Had the stack been empty prior to the put() call, the postcondition at line 42 in Listing 1 would be violated too. Here is the error message that would report:

Postcondition violated: !obj().empty() at dbc.test.StackImpl.put

The supplier is also responsible for the class invariant. To see what happens when an invariant is violated, you could change line 30 in Listing 2 to count() == 1. This will violate the invariant declared at line 6 in Listing 1. When the following client code executes:

Stack stack = (Stack)DBC.newInstance(new StackImpl(10));

the following error message will indicate a violated invariant:

Invariant violated: obj().empty() == (obj.count() == 0) at
dbc.test.StackImpl

As mentioned earlier, no assertions were declared in StackImpl, but the assertions declared in Stack were still enforced. This is an important concept to understand. A descendent cannot break the contract established by its ascendants. However, that does not mean StackImpl cannot have its own assertions; it may, as long as it fulfills the contract specified by Stack.

Figure 4 illustrates steps that occur when the client calls method put().

Figure 4. Method put() is called. Click on thumbnail to view full-size image.

Figure 4 illustrates the following sequence of steps:

  1. The client calls stack.put().
  2. A dynamic proxy intercepts the call and delegates it to DBC.invoke(). Method DBC.invoke() is the dynamic proxy's invocation handler.
  3. DBC.invoke() checks the preconditions with the help of naming conventions and Java reflection.
  4. DBC.invoke() calls the primary object (StackImpl.put).
  5. DBC.invoke() checks the postconditions with the help of naming conventions and Java reflection.
  6. DBC.invoke() checks the invariants.

Separate objects

As described earlier, preconditions have an optional wait statement, which is used in Listing 1 at line 23 and line 41 for methods item() and put(), respectively. This wait statement has no effect under regular circumstances; line 23 and 41 act as regular preconditions. For example, if the client calls method item() when the stack is empty, a precondition violation will occur, as the precondition states. If, however, we create the stack object as a separate object, the preconditions at line 23 and 41 would turn into wait statements. These statements will wait until the precondition is true.

The wait statements become relevant in situations of concurrent access. For instance, suppose the stack object is accessed from multiple threads. Suppose one thread reads (stack.item()), while another thread writes (stack.put(Object)). In Java, to achieve thread safety, you use the keyword synchronized. In the Stack example, we would implement the method item() as follows:

public synchronized Object item()
{
  while (!empty())
  wait()
  return 'top object';
}

Notice that item() caller(s) must wait until the stack isn't empty, as the precondition for item() states. To use preconditions as wait statements, you must be able to tell the DBC runtime environment that multiple threads will use the object. The DBC runtime environment needs to know that the object is separate. You can show that when you construct the object. The class dbc.DBC has an additional method: public static Object newInstance(Object obj, boolean separate). If the second argument separate in the newInstance() method above is true, the DBC runtime will do the following:

  • Protect each method on the primary object by using Java's keyword synchronized
  • Every precondition that has a wait statement after the Boolean statement will wait until that precondition is true (in the worst case, it waits forever)
  • Since we use some preconditions as wait statements rather than to check correctness, they are always turned on, and cannot be turned off

By adding the wait statement to the appropriate preconditions, you create a stack that you can use in a single-threaded environment as well as a multithreaded environment. Because preconditions are part of the stack specification and not its implementation, any dbc.test.Stack implementation will work in a single-threaded environment as well as a multithreaded environment.

Final thoughts: Importance of interfaces

In this article, we utilized DBC in Java by leveraging the following existing Java technologies:

  • Dynamic proxies and reflection for the DBC runtime environment
  • Javadoc and its Doclet API to generate assertion classes

Hopefully, this article has inspired you to try DBC, or at least think of developing software in terms of contracts between clients and suppliers. A DBC way of thinking is a great tool for developing high quality software. Additionally, DBC may even enhance your object-oriented analysis and design skills.

You can use the DBCProxy framework not only during design and development phases, but also during testing phases. The overhead of using the framework is minor. However, I don't recommend that you use the framework in a production system. The DBCProxy framework intends to aid in developing high quality software. It uses the Proxy pattern, while leveraging JDK 1.3's new dynamic proxy feature, as a means to execute assertions.

As I mentioned earlier, the DBCProxy framework will only work when objects are referenced within the interfaces they implement. This means that every DBC-enabled object must be based on at least one interface, and only methods that have been declared in an interface can be DBC-enabled. This is a consequence and limitation of dynamic proxies. However, it might not be a serious limitation since, in general, using interfaces in code is considered good design.

Anders Eliasson has more than 12 years' experience in software development and has been programming in Java since 1995. Anders is a Java 2 Certified Programmer and Java 2 Certified Developer. An event that solidified the role of DBC in his software development was a one-week object-oriented course with Bertrand Meyer. Anders would like to thank Charlie Hunt for his help reviewing this article.

Learn more about this topic

Join the discussion
Be the first to comment on this article. Our Commenting Policies
See more