Precondition and postcondition in Java

Question

Question that makes me think:

when we speak of precondition in a method we refer to a condition verified by the method itself(1) or to a condition verified by the caller(2)? for example

(1)
    ...
    withdrawal(100);
}

void withdrawal(int v)
{
    if (v<balance)
        balance-=v;
    else
        throw new exception;
}

(2)
    ...
    if (getBalance()>100)
        withdrawal(100);
    else
        throw new exception;
}

void withdrawal(int v)
{
    balance-=v;
}

The same for the postcondition?

Answer 1

Both are verified in the method itself.

For advice on programming pre and post conditions in Java, see: https://docs.oracle.com/javase/8/docs/technotes/guides/language/assert.html#usage-conditions

You may also be interested in the Wikipedia article on design by contract. Note that pre and post conditions are implemented differently in different languages, and that in languages without first-class support for DbC (like Java) you may use plugins or tooling to assist in the enforcement of contracts. For example, annotations could be another approach in Java.

Without the aid of additional tools, preconditions are simply implemented as guard clauses, in a defensive programming style. In Java, null checks enforce a ubiquitous precondition.