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:

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