Contract Programming

Contracts are compiled out with -release (or controlled with -check=in=off, etc.).

In inheritance: preconditions are OR'd (they may loosen) and postconditions are AND'd (they may tighten), following the Liskov substitution principle.

int divide(int a, int b)
in (b != 0, "divisor must be non-zero")             // precondition (expression form)
out (result; result * b <= a)                       // postcondition
{
    return a / b;
}

double sqrtChecked(double x)
in
{
    assert(x >= 0);
}
out (r)
{
    assert(r >= 0);
}
do
{
    import std.math : sqrt;
    return sqrt(x);
}

class BankAccount
{
    private double balance = 0;

    invariant { assert(balance >= 0, "balance can't be negative"); }   // checked around public methods

    void withdraw(double amt)
    in (amt > 0)
    {
        balance -= amt;
    }
}