Featured White Papers

• Why choose an Open Source BPM?
• 10 FAQs on Business Process Management
• Best Practices for Getting Started with BPM
• Free Your Devs From The Pain Of Java Redeploys
• Increase Velocity 40% by Using JRebel
• What Developers Want: The End of Application Redeploys
• Developer Productivity Report: Java Tools, Tech, Devs, and Data
• Coding with JRebel: Java Forever Changed
• Utilizing Fast Testing to Transform Java Development
• Do You Really Get Classloaders?
• Pragmatic Continuous Delivery with Jenkins, Nexus, and LiveRebel
• Your Next Java Web App: Less XML, No Long Restarts, Fewer Hassles
• Coding with JRebel, Java Forever Changed
• 2012 Developer Productivity Report: Java Tools, Tech, Devs, and Data

Sponsored Links

• APIs for Java Programmers: Manage & Convert DOC, XLS, PPT, PDF & More

• Instantly Preview Java Code Changes: JRebel.com

Sponsored Links

Optimize with a SATA RAID Storage Solution
Range of capacities as low as $1250 per TB. Ideal if you currently rely on servers/disks/JBODs

Implement Design by Contract for Java using dynamic proxies

Write bug-free code with the DBCProxy framework

By Anders Eliasson, JavaWorld.com, 02/15/02

Page 4 of 5

/**
* @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.