Class invariant example

Here follows an example of a class invariant contract, and how contracts are tied to their targets:

  @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;
    }
  }
  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 contract is tied to the target using an annotation. The contract has a constructor that takes an argument of the target type.
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.