Reputation: 11
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?
Upvotes: -3
Views: 1235
Reputation: 17066
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.
Upvotes: 2