mirrors/eiffel-org
1
0
Fork 0
mirror of https://github.com/EiffelSoftware/eiffel-org.git synced 2026-02-11 04:55:14 +01:00
Code Issues Packages Projects Releases Wiki Activity

Author:halw

Browse Source 
Date:2009-10-05T20:55:29.000000Z


git-svn-id: https://svn.eiffel.com/eiffel-org/trunk@320 abb3cda0-5349-4a8f-a601-0c33ac3a8c38
This commit is contained in:
halw
2009-10-05 20:55:29 +00:00
parent bb8ce730c0
commit 9e59f56200
2 changed files with 45 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

5
documentation/current/method/eiffel-tutorial-et/et-design-contract-tm-assertions-and-exceptions.wiki
View File

@@ -90,8 +90,12 @@ Each assertion is made of one or more subclauses, each of them a boolean express
Because assertions benefit from the full power of boolean expressions, they may include function calls. This makes it possible to express sophisticated consistency conditions, such as " the graph contains no cycle", which would not be otherwise expressible through simple expressions, or even through first-order predicate calculus, but which are easy to implement as Eiffel functions returning boolean results.
===Preconditions===
The precondition of a routine expresses conditions that the routine is imposing on its clients. Here a call to <code>deposit</code> is correct if and only if the value of the argument is non-negative. The routine does not guarantee anything for a call that does not satisfy the precondition. It is in fact part of the Eiffel method that a routine body should '''never''' test for the precondition, since it is the client's responsibility to ensure it. (An apparent paradox of Design by Contract&#153;, which is reflected in the bottom-right entries of the preceding and following contract tables, and should not be a paradox any more at the end of this discussion, is that one can get more reliable software by having fewer explicit checks in the software text.)
===Postconditions===
The postcondition of a routine expresses what the routine guaranteed to its clients for calls satisfying the precondition. The notation <code>old expression</code>, valid in postconditions ( <code>ensure</code> clauses) only, denotes the value that <code>expression</code> had on entry to the routine.
The precondition and postcondition state the terms of the contract between the routine and its clients, similar to the earlier example of a human contract:
@@ -116,6 +120,7 @@ Update deposits list and balance.
No need to handle negative arguments.
|}
===Class invariants===
The class invariant, as noted, applies to all features. It must be satisfied on exit by any creation procedure, and is implicitly added to both the precondition and postcondition of every exported routine. In this respect it is both good news and bad news for the routine implementer: good news because it guarantees that the object will initially be in a stable state, averting the need in the example to check that the total of <code>all_deposits</code> is compatible with the <code>balance</code>; bad news because, in addition to its official contract as expressed by its specific postcondition, every routine must take care of restoring the invariant on exit.