11.6: Contracts for SW Reliability
By associating clauses ‘require <pre>’ and ‘ensure <post>’ with a routine A, the class tells its clients (in Eiffel):
“If you promise to call r with <pre> satisfied, then in return, I promise to deliver a final state in which <post> is satisfied.”
The supplier of A does not have to check that the pre-conditions are valid
(except to debug the clients’ code - RJL).