Interface example

Here is an example of a contract defined for an interface:

  @ContractReference(contractClassName = "DummyContract")
  public interface Dummy
  {
    double divide(double x, double y);
  }

  public class DummyContract extends ContractBase<Dummy>
  {
    public DummyContract(Dummy target)
    {
      super(target);
    }

    public void pre_divide(double x, double y)
    {
      assert y != 0;
    }

    public void post_divide(double x, double y)
    {
      assert getReturnValue() == x / y;
    }
  }

The contract will verify that all usages of the divide interface meets the pre condition, and that all implementations of the interface will meet the post condition.