JPDBC in nutshell

Main features

• no need to use preprocessors or java-agents
• primary target in unit/component tests
• contracts are defined with annotations: @Invariant, @Pre, @Post
• contracts are evaluated using reflection and JavaScript engine
• contracts can be evaluated for mock-objects

---

Simple example 1/2

In the following example MyManager uses interface MyInterface, but the implementor of MyManager has not honoured the contract @Pre("!=null"). (Fix for this could be e.g. using Google Guava's Strings.nullToEmpty in the callDo)

(Imports are not showed in the following snippets to save vertical space)

public interface MyInterface {
    @Post("result == 'success' || result == 'failure'")
    String doIt(@Pre("!=null") String text);
}

MyInterface.java

public class MyManager {
    private final MyInterface myInterface;
    public MyManager(MyInterface myInterface) {
        this.myInterface = myInterface;
    }
    public void callDo(String text) {
        myInterface.doIt(text);
    }
}

MyManager.java

public class MyManagerTest extends EasyMockSupportWithDbC {
    @Test
    public void test() {
        MyInterface myInterface = createNiceMock(MyInterface.class);
        MyManager myManager = new MyManager(myInterface);
        replayAll();
        myManager.callDo(null);  // this will throw PreconditionException
        verifyAll();
    }
}

MyManagerTest.java

---

Simple example 2/2

Also the implementor of MyInterface has been lazy, and has not honoured the postcondition @Post("result == 'success' || result == 'failure'").

public class MyObject implements MyInterface {
    @Override
    public String doIt(String text) {
        if (text.equals("password")) {
            return "success";
        }
        return "";
    }
}

MyObject.java

public class MyObjectTest extends DbCSupportImpl {
    @Test
    public void test() {
        MyObject myObject = dbc(new MyObject());
        myObject.doIt("password");
        myObject.doIt("teststring");  // this will throw PostconditionException
    }
}

MyObjectTest.java

---

How it all works

Basics

Contracts are evaluated in the following order:
1. @Invariant (class invariant)
2. @Pre (precondition) for method
3. @Pre for arguments
4. @Post (postcondition)
5. and finally @Invariant again (this last one is evaluated in actual finally-block; even though the method throws, the class invariant should hold).

The actual contract is written in the value of the annotation, e.g.

@Invariant("size() >= 0")
public class Stack {
    ...
    public int size() {
        ...
    }
}

When writing precondition for argument, you can use word "arg" to refer to value of the argument:

public class Stack {
    ...
    public void push(@Pre("arg != null && !arg.isEmpty()") String data) {
        ...
    }
}

For postcondition, "result" refers to the return value of the method.

If the contract in @Pre for argument starts with a relational operator (==, !=, <=, >=, <, >), the contract is appended with "arg".
If the contract in @Post starts with a relational operator, the contract is appended with "result".

Contract evaluation

1. All method invocations inside the contract are evaluated using reflection; is there is no "root" object defined ("arg" or "result"), the method is searched from the interface of "this" object. Method invocations can be chained if needed, and only zero-argument methods are currently supported. See Listing 1.

2. After the method invocations are resolved, the return values are feeded into JavaScript (JS) engine, invocations are replaced with the corresponding variable names, and the contract is evaluated in the JS engine. If contract consists of multiple JS lines (separated by semicolon), the last one should be without semicolon and evaluate as the actual outcome of the contract. The outcome should be boolean.

3. One JS engine context is used for exactly one method call; this allows you to forward data from one contract to another. See Listing 2.

Since the evaluating step 2 is done in JavaScript, the equal comparison for strings can be done with "==".

@Post("result.size() > 0 && result.get(0).toLowerCase() == 'text'")
public List<String> getList();

Listing 1.

@Pre("var origdamage=health(); true")
@Post("origdamage - damage == health()")
void sufferDamage(@Pre("var damage = arg; damage >= 0") int damage);

int health();

Listing 2.