Examples

Here is a list of examples, to get you started:

Class Invariants
Pre and Post Conditions
Accessing Private Target Members

Class Invariants

The target class, which will be contracted

@ContractReference(contractClassName = "DummyContract")
public class Dummy {
    protected double m_divisor;
        
    public Dummy(double divisor) {
        m_divisor = divisor;
    }
        
    public double divide(double x) {
        return x / m_divisor;
    }
}

and it's contract class

public class DummyContract {
    Dummy m_target;
    
    public DummyContract(Dummy target) {
        m_target = target;
    }
        
    public void classInvariant() {
        assert m_target.m_divisor != 0;
    }
}

The assumption made in the Dummy class constructor is that parameter divisor is never 0. This is verified by the classInvariant method in the DummyContract class.

The contractClassName attribute of the ContractReference annotation does not have to be fully qualified if the contract class is implemented in the same package as the target class.

Pre and Post Conditions

The target class

@ContractReference(contractClassName = "DummyContract")
public class Dummy {
    protected List m_stuff = new LinkedList();
        
    public int addItem(Object item) {
        m_stuff.add(item);
        return m_stuff.size();
    }
}

and it's contract

public class DummyContract extends ContractBase<Dummy> {
    public DummyContract(Dummy target) {
        super(target);
    }
    
    public void classInvariant() {
        assert m_target.m_stuff != null;
    }
    
    public void pre_addItem(Object item) {
        assert item != null;
        super.setPreconditionValue("list-size", m_target.m_stuff.size());
    }
    
    public void post_addItem(Object item) {
        assert m_target.m_stuff.contains(item);
        int preSize = super.getPreconditionValue("list-size");
        assert preSize == m_target.m_stuff.size() - 1;
        assert m_target.m_stuff.size() == super.getReturnValue();
    }
}

The pre condition checks for null arguments and by extending the ContractBase class, the post condition verifies both that the item actually has been added, that nothing else has been removed, and that the return value is the expected.

Accessing Private Target Members

If you pass in the target reference to the ContractBase constructor, you will be able to get access to private fields in the target using the ContractBase.getTargetField(String fieldName) method, as shown below:

public class SomeContract extends ContractBase<Some> {
    public SomeContract(Some target) {
        super(target);
    }
    
    public void classInvariant() {
        assert ((List)super.getTargetField("m_stuff")).size() > 0;
        assert ((List)super.getTargetField("m_stuff")).get(0).equals("boho");
    }
}