That is, the redefined routine may increase the benefits it provides to the client, but may not decrease those benefits. See also Precondition Design by contract Hoare logic Invariants maintained by conditions Database trigger References Programming constructs Formal methods Logic in computer science Mathematics of computing Articles with example Eiffel code