Pre condition example

Here follows an example of a pre condition contract:

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

  public class DummyContract
  {
    public void classInvariant()
    {
      // Nothing to do here
    }

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

The assumption made in the divide is that parameter y is never 0. This is verified by the pre_divide method..