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..