mirror of
https://github.com/EiffelSoftware/eiffel-org.git
synced 2025-12-06 14:52:03 +01:00
Author:halw
Date:2008-10-19T17:24:57.000000Z git-svn-id: https://svn.eiffel.com/eiffel-org/trunk@89 abb3cda0-5349-4a8f-a601-0c33ac3a8c38
This commit is contained in:
halw
@@ -36,9 +36,9 @@ In addition to preconditions and postconditions, contract clauses include '''cla
|
||||
|
||||
==Expressing assertions==
|
||||
|
||||
Eiffel provides syntax for expressing preconditions ( <code> require </code>), postconditions ( <code> ensure </code>) and class invariants ( <code> invariant </code>), as well as other assertion constructs studied later (see [[10 Other Mechanisms|"Instructions", page 84]] ): loop invariants and variants, check instructions.
|
||||
Eiffel provides syntax for expressing preconditions ( <code>require</code>), postconditions ( <code>ensure</code>) and class invariants ( <code>invariant</code>), as well as other assertion constructs studied later (see [[10 Other Mechanisms|"Instructions", page 84]] ): loop invariants and variants, check instructions.
|
||||
|
||||
Here is a partial update of class <code> ACCOUNT </code> with more assertions:
|
||||
Here is a partial update of class <code>ACCOUNT</code> with more assertions:
|
||||
<code>
|
||||
indexing
|
||||
description: "Simple bank accounts"
|
||||
@@ -84,13 +84,13 @@ invariant
|
||||
end -- class ACCOUNT
|
||||
</code>
|
||||
|
||||
Each assertion is made of one or more subclauses, each of them a boolean expression (with the additional possibility of the <code> old </code> construct). The effect of including more than one sub clause, as in the postcondition of <code> deposit </code> and in the invariant, is the same as connecting them through an <code> and </code>. Each clause may be preceded by a label, such as <code> consistent_balance </code> in the invariant, and a colon; the label is optional and does not affect the assertion's semantics, except for error reporting as explained in the next section, but including it systematically is part of the recommended style. The value of the boolean expression <code> a implies b </code> is true except if <code> a </code> is true and <code> b </code> false.
|
||||
Each assertion is made of one or more subclauses, each of them a boolean expression (with the additional possibility of the <code>old</code> construct). The effect of including more than one sub clause, as in the postcondition of <code>deposit</code> and in the invariant, is the same as connecting them through an <code>and</code>. Each clause may be preceded by a label, such as <code>consistent_balance</code> in the invariant, and a colon; the label is optional and does not affect the assertion's semantics, except for error reporting as explained in the next section, but including it systematically is part of the recommended style. The value of the boolean expression <code>a implies b</code> is true except if <code>a</code> is true and <code>b</code> false.
|
||||
|
||||
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.
|
||||
|
||||
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™, 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.)
|
||||
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™, 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.)
|
||||
|
||||
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 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:
|
||||
{| border="1"
|
||||
@@ -112,18 +112,18 @@ Update deposits list and balance.
|
||||
No need to handle negative arguments.
|
||||
|}
|
||||
|
||||
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.
|
||||
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.
|
||||
|
||||
A requirement on meaningful contracts is that they should be in good faith: satisfiable by an honest partner. This implies a consistency rule: if a routine is exported to a client (either generally or selectively), any feature appearing in its precondition must also be available to that client. Otherwise -- for example if the precondition included <code> require n > 0 </code>, where <code> n </code> is a secret attribute -- the supplier would be making demands that a good-faith client cannot possibly check for.
|
||||
A requirement on meaningful contracts is that they should be in good faith: satisfiable by an honest partner. This implies a consistency rule: if a routine is exported to a client (either generally or selectively), any feature appearing in its precondition must also be available to that client. Otherwise -- for example if the precondition included <code>require n > 0</code>, where <code>n</code> is a secret attribute -- the supplier would be making demands that a good-faith client cannot possibly check for.
|
||||
|
||||
Note in this respect that guaranteeing a precondition does not necessarily mean, for the client, testing for it. Assuming <code> n </code> is exported, a call may test for the precondition
|
||||
Note in this respect that guaranteeing a precondition does not necessarily mean, for the client, testing for it. Assuming <code>n</code> is exported, a call may test for the precondition
|
||||
<code>
|
||||
if x.n > 0 then x.r end
|
||||
</code>
|
||||
|
||||
possibly with an <code> else </code> part. But if the context of the call, in the client's code, implies that <code> n </code> is positive -- perhaps because some preceding call set it to the sum of two squares -- then there is no need for an <code> if </code> or similar construct.
|
||||
possibly with an <code>else</code> part. But if the context of the call, in the client's code, implies that <code>n</code> is positive -- perhaps because some preceding call set it to the sum of two squares -- then there is no need for an <code>if</code> or similar construct.
|
||||
|
||||
{{note|In such a case, a <code> check </code> instruction as introduced later ( [[10 Other Mechanisms|"Instructions", page 84]] ) is recommended if the reason for omitting the test is non-trivial. }}
|
||||
{{note|In such a case, a <code>check</code> instruction as introduced later ( [[10 Other Mechanisms|"Instructions", page 84]] ) is recommended if the reason for omitting the test is non-trivial. }}
|
||||
|
||||
==Using contracts for built-in reliability==
|
||||
|
||||
@@ -135,7 +135,7 @@ This simple observation -- usually not clear to people until they have practiced
|
||||
|
||||
Contracts in Eiffel are not just wishful thinking. They can be monitored at run time under the control of compilation options.
|
||||
|
||||
It should be clear from the preceding discussion that contracts are not a mechanism to test for special conditions, for example erroneous user input. For that purpose, the usual control structures ( <code> if deposit_sum > 0 then </code> ...) are available, complemented in applicable cases by the exception handling mechanism reviewed next. An assertion is instead a '''correctness condition''' governing the relationship between two software modules (not a software module and a human, or a software module and an external device). If <code> sum </code> is negative on entry to <code> deposit </code>, violating the precondition, the culprit is some other software element, whose author was not careful enough to observe the terms of the deal. Bluntly:
|
||||
It should be clear from the preceding discussion that contracts are not a mechanism to test for special conditions, for example erroneous user input. For that purpose, the usual control structures ( <code>if deposit_sum > 0 then</code> ...) are available, complemented in applicable cases by the exception handling mechanism reviewed next. An assertion is instead a '''correctness condition''' governing the relationship between two software modules (not a software module and a human, or a software module and an external device). If <code>sum</code> is negative on entry to <code>deposit</code>, violating the precondition, the culprit is some other software element, whose author was not careful enough to observe the terms of the deal. Bluntly:
|
||||
|
||||
{{note| '''Assertion Violation rule '''A run-time assertion violation is the manifestation of a bug. }}
|
||||
|
||||
@@ -147,26 +147,26 @@ To be more precise: <br/>
|
||||
That violations indicate bugs explains why it is legitimate to enable or disable assertion monitoring through mere compilation options: for a correct system -- one without bugs -- assertions will always hold, so the compilation option makes no difference to the semantics of the system.
|
||||
|
||||
But of course for an incorrect system the best way to find out where the bug is -- or just that there is a bug -- is often to monitor the assertions during development and testing. Hence the presence of the compilation options, which EiffelStudio lets you set separately for each class, with defaults at the system and cluster levels: <br/>
|
||||
* <code> no </code> : assertions have no run-time effect.
|
||||
* <code> require </code> : monitor preconditions only, on routine entry.
|
||||
* <code> ensure </code> : preconditions on entry, postconditions on exit.
|
||||
* <code> invariant </code> : like <code> ensure </code>, plus class invariant on both entry and exit for qualified calls.
|
||||
* <code> all </code> : like <code> invariant </code>, plus <code> check </code> instructions, loop invariants and loop variants ( [[10 Other Mechanisms|"Exception handling", page 46]] ).
|
||||
* <code>no</code> : assertions have no run-time effect.
|
||||
* <code>require</code> : monitor preconditions only, on routine entry.
|
||||
* <code>ensure</code> : preconditions on entry, postconditions on exit.
|
||||
* <code>invariant</code> : like <code>ensure</code>, plus class invariant on both entry and exit for qualified calls.
|
||||
* <code>all</code> : like <code>invariant</code>, plus <code>check</code> instructions, loop invariants and loop variants ( [[10 Other Mechanisms|"Exception handling", page 46]] ).
|
||||
|
||||
|
||||
An assertion violation, if detected at run time under one of these options other than the first, will cause an exception ( [[8 Design by Contract (tm), Assertions and Exceptions|"Instructions", page 84]] ). Unless the software has an explicit "retry" plan as explained in the discussion of exceptions, the violation will cause produce an exception trace and cause termination (or, in EiffelStudio, a return to the environment's browsing and debugging facilities at the point of failure). If present, the label of the violated sub clause will be displayed, to help identify the problem.
|
||||
|
||||
The default is <code> require </code>. This is particularly interesting in connection with the Eiffel method's insistence on reuse: with libraries such as EiffelBase, richly equipped with preconditions expressing terms of use, an error in the '''client software''' will often lead, for example through an incorrect argument, to violating one of these preconditions. A somewhat paradoxical consequence is that even an application developer who does not apply the method too well (out of carelessness, haste, indifference or ignorance) will still benefit from the presence of contracts in someone else's library code.
|
||||
The default is <code>require</code>. This is particularly interesting in connection with the Eiffel method's insistence on reuse: with libraries such as EiffelBase, richly equipped with preconditions expressing terms of use, an error in the '''client software''' will often lead, for example through an incorrect argument, to violating one of these preconditions. A somewhat paradoxical consequence is that even an application developer who does not apply the method too well (out of carelessness, haste, indifference or ignorance) will still benefit from the presence of contracts in someone else's library code.
|
||||
|
||||
During development and testing, assertion monitoring should be turned on at the highest possible level. Combined with static typing and the immediate feedback of compilation techniques such as the Melting Ice Technology, this permits the development process mentioned in the section [[3 The Software Process in Eiffel|"Quality and functionality", page 10]] , where errors are exterminated at birth. No one who has not practiced the method in a real project can imagine how many mistakes are found in this way; surprisingly often, a violation will turn out to affect an assertion that was just included for goodness' sake, the developer being convinced that it could never "possibly" fail to be satisfied.
|
||||
|
||||
By providing a precise reference (the description of what the software is supposed to do) against which to assess the reality (what the software actually does), Design by Contract™ profoundly transforms the activities of debugging, testing and quality assurance.
|
||||
|
||||
When releasing the final version of a system, it is usually appropriate to turn off assertion monitoring, or bring it down to the <code> require </code> level. The exact policy depends on the circumstances; it is a trade off between efficiency considerations, the potential cost of mistakes, and how much the developers and quality assurance team trust the product. When developing the software, however, you should always assume -- to avoid loosening your guard -- that in the end monitoring will be turned off.
|
||||
When releasing the final version of a system, it is usually appropriate to turn off assertion monitoring, or bring it down to the <code>require</code> level. The exact policy depends on the circumstances; it is a trade off between efficiency considerations, the potential cost of mistakes, and how much the developers and quality assurance team trust the product. When developing the software, however, you should always assume -- to avoid loosening your guard -- that in the end monitoring will be turned off.
|
||||
|
||||
==The contract form of a class==
|
||||
|
||||
Another application of assertions governs documentation. Environment mechanisms, such as clicking the <code> Form Contract </code> icon in Eiffelstudio, will produce, from a class text, an abstracted version which only includes the information relevant for client authors. Here is the contract form of class <code> ACCOUNT </code> in the latest version given:
|
||||
Another application of assertions governs documentation. Environment mechanisms, such as clicking the <code>Form Contract</code> icon in Eiffelstudio, will produce, from a class text, an abstracted version which only includes the information relevant for client authors. Here is the contract form of class <code>ACCOUNT</code> in the latest version given:
|
||||
<code>
|
||||
indexing
|
||||
description: "Simple bank accounts"
|
||||
@@ -198,7 +198,7 @@ invariant
|
||||
end -- class interface ACCOUNT
|
||||
</code>
|
||||
|
||||
The words <code> interface class </code> are used instead of just <code> class </code> to avoid any confusion with actual Eiffel text, since this is documentation, not executable software. (It is in fact possible to generate a compilable variant of the Contract Form in the form of a deferred class, a notion defined later.)
|
||||
The words <code>interface class</code> are used instead of just <code>class</code> to avoid any confusion with actual Eiffel text, since this is documentation, not executable software. (It is in fact possible to generate a compilable variant of the Contract Form in the form of a deferred class, a notion defined later.)
|
||||
|
||||
Compared to the full text, the Contract Form of a class (also called its "short form") retains all its interface properties, relevant to client authors: <br/>
|
||||
* Names and signatures (argument and result type information) for exported features.
|
||||
@@ -207,9 +207,9 @@ Compared to the full text, the Contract Form of a class (also called its "short
|
||||
* Class invariant (same observation).
|
||||
|
||||
|
||||
The following elements, however, are not in the Contract Form: any information about non-exported features; all the routine bodies ( <code> do </code> clauses, or the <code> external </code> and <code> once </code> variants seen in [[5 The Static Picture: System Organization|"External software", page 16]] above and [[10 Other Mechanisms|"Once routines and shared objects", page 82]] below); assertion subclauses involving non-exported features; and some keywords not useful in the documentation, such as <code> is </code> for a routine.
|
||||
The following elements, however, are not in the Contract Form: any information about non-exported features; all the routine bodies ( <code>do</code> clauses, or the <code>external</code> and <code>once</code> variants seen in [[5 The Static Picture: System Organization|"External software", page 16]] above and [[10 Other Mechanisms|"Once routines and shared objects", page 82]] below); assertion subclauses involving non-exported features; and some keywords not useful in the documentation, such as <code>is</code> for a routine.
|
||||
|
||||
In accordance with the Uniform Access principle (page [[6 The Dynamic Structure: Execution Model|19]] ), the Contract Form does not distinguish between attributes and argument-less queries. In the above example, <code> balance </code> could be one or the other, as it makes no difference to clients, except possibly for performance.
|
||||
In accordance with the Uniform Access principle (page [[6 The Dynamic Structure: Execution Model|19]] ), the Contract Form does not distinguish between attributes and argument-less queries. In the above example, <code>balance</code> could be one or the other, as it makes no difference to clients, except possibly for performance.
|
||||
|
||||
The Contract Form is the fundamental tool for using supplier classes in the Eiffel method. It enables client authors to reuse software elements without having to read their source code. This is a crucial requirement in large-scale industrial developments.
|
||||
|
||||
@@ -227,14 +227,14 @@ The Contract Form -- or its variant the Flat-Contract Form, which takes account
|
||||
Another application of Design by Contract™ governs the handling of unexpected cases. The vagueness of many discussions of this topic follows from the lack of a precise definition of terms such as "exception". With Design by Contract™ we are in a position to be specific: <br/>
|
||||
* Any routine has a contract to achieve.
|
||||
* Its body defines a strategy to achieve it -- a sequence of operations, or some other control structure involving operations. Some of these operations are calls to routines, with their own contracts; but even an atomic operation, such as the computation of an arithmetic operation, has an implicit contract, stating that the result will be representable.
|
||||
* Any one of these operations may <code> fail </code>, that is to say be unable to meet its contract; for example an arithmetic operation may produce an overflow (a on-representable result).
|
||||
* Any one of these operations may <code>fail</code>, that is to say be unable to meet its contract; for example an arithmetic operation may produce an overflow (a on-representable result).
|
||||
* The failure of an operation is an '''exception''' for the routine that needed the operation.
|
||||
* As a result the routine may fail too -- causing an exception in its own caller.
|
||||
|
||||
|
||||
Note the precise definitions of the two key concepts, failure and exception. Although failure is the more basic one -- since it is defined for atomic, non-routine operations -- the definitions are mutually recursive, since an exception may cause a failure of the recipient routine, and a routine's failure causes an exception in its own caller.
|
||||
|
||||
Why state that an exception "may" cause a failure? It is indeed possible to "rescue" a routine from failure in the case of an exception, by equipping it with a clause labeled <code> rescue </code>, as in:
|
||||
Why state that an exception "may" cause a failure? It is indeed possible to "rescue" a routine from failure in the case of an exception, by equipping it with a clause labeled <code>rescue</code>, as in:
|
||||
<code>
|
||||
read_next_character (f: FILE) is
|
||||
-- Make next character available in last_character.
|
||||
@@ -255,9 +255,9 @@ read_next_character (f: FILE) is
|
||||
end
|
||||
</code>
|
||||
|
||||
This example includes the only two constructs needed for exception handling: <code> rescue </code> and <code> retry </code>. A <code> retry </code> instruction is only permitted in a rescue clause; its effect is to start again the execution of the routine, without repeating the initialization of local entities (such as <code> impossible </code> in the example, which was initialized to <code> False </code> on first entry). Features <code> failed </code> and <code> last_character </code> are assumed to be attributes of the enclosing class.
|
||||
This example includes the only two constructs needed for exception handling: <code>rescue</code> and <code>retry</code>. A <code>retry</code> instruction is only permitted in a rescue clause; its effect is to start again the execution of the routine, without repeating the initialization of local entities (such as <code>impossible</code> in the example, which was initialized to <code>False</code> on first entry). Features <code>failed</code> and <code>last_character</code> are assumed to be attributes of the enclosing class.
|
||||
|
||||
This example is typical of the use of exceptions: as a last resort, for situations that should not occur. The routine has a precondition, <code> file.readable </code>, which ascertains that the file exists and is accessible for reading characters. So clients should check that everything is fine before calling the routine. Although this check is almost always a guarantee of success, a rare combination of circumstances could cause a change of file status (because a user or some other system is manipulating the file) between the check for <code> readable </code> and the call to <code> low_level_read_function </code>. If we assume this latter function will fail if the file is not readable, we must catch the exception.
|
||||
This example is typical of the use of exceptions: as a last resort, for situations that should not occur. The routine has a precondition, <code>file.readable</code>, which ascertains that the file exists and is accessible for reading characters. So clients should check that everything is fine before calling the routine. Although this check is almost always a guarantee of success, a rare combination of circumstances could cause a change of file status (because a user or some other system is manipulating the file) between the check for <code>readable</code> and the call to <code>low_level_read_function</code>. If we assume this latter function will fail if the file is not readable, we must catch the exception.
|
||||
|
||||
A variant would be
|
||||
<code>
|
||||
@@ -275,9 +275,9 @@ rescue
|
||||
end
|
||||
</code>
|
||||
|
||||
which would try again up to <code> Max_attempts </code> times before giving up.
|
||||
which would try again up to <code>Max_attempts</code> times before giving up.
|
||||
|
||||
The above routine, in either variant, never fails: it always fulfills its contract, which states that it should either read a character or set <code> failed </code> to record its inability to do so. In contrast, consider the new variant
|
||||
The above routine, in either variant, never fails: it always fulfills its contract, which states that it should either read a character or set <code>failed</code> to record its inability to do so. In contrast, consider the new variant
|
||||
<code>
|
||||
local
|
||||
attempts: INTEGER
|
||||
@@ -291,27 +291,27 @@ rescue
|
||||
end
|
||||
</code>
|
||||
|
||||
with no more role for <code> failed </code>. In this case, after <code> Max_attempts </code> unsuccessful attempts, the routine will execute its <code> rescue </code> clause to the end, with no <code> retry </code> (the <code> if </code> having no <code> else </code> clause). This is how a routine '''fails'''. It will, as noted, pass on the exception to its caller.
|
||||
with no more role for <code>failed</code>. In this case, after <code>Max_attempts</code> unsuccessful attempts, the routine will execute its <code>rescue</code> clause to the end, with no <code>retry</code> (the <code>if</code> having no <code>else</code> clause). This is how a routine '''fails'''. It will, as noted, pass on the exception to its caller.
|
||||
|
||||
Such a rescue clause should, before terminating, restore the invariant of the class so that the caller and possible subsequent <code> retry </code>attempts from higher up find the objects in a consistent state. As a result, the rule for an absent <code> rescue </code> clause -- the case for the vast majority of routines in most systems -- is that it is equivalent to
|
||||
Such a rescue clause should, before terminating, restore the invariant of the class so that the caller and possible subsequent <code>retry</code>attempts from higher up find the objects in a consistent state. As a result, the rule for an absent <code>rescue</code> clause -- the case for the vast majority of routines in most systems -- is that it is equivalent to
|
||||
<code>
|
||||
rescue
|
||||
default_rescue
|
||||
</code>
|
||||
|
||||
where procedure <code> default_rescue </code> comes from <code> ANY </code>, where it is defined to do nothing; in a system built for robustness, classes subject to non-explicitly-rescued exceptions should redefine <code> default_rescue </code> (perhaps using a creation procedure, which is bound by the same formal requirement) so that it will always restore the invariant.
|
||||
where procedure <code>default_rescue</code> comes from <code>ANY</code>, where it is defined to do nothing; in a system built for robustness, classes subject to non-explicitly-rescued exceptions should redefine <code>default_rescue</code> (perhaps using a creation procedure, which is bound by the same formal requirement) so that it will always restore the invariant.
|
||||
|
||||
Behind Eiffel's exception handling scheme lies the principle -- at first an apparent platitude, but violated by many existing mechanisms -- that a routine should '''either succeed or fail'''. This is in turn a consequence of Design by Contract™ principles: succeeding means being able to fulfill the contract, possibly after one or more <code> retry </code>; failure is the other case, which must always trigger an exception in the caller. Otherwise it would be possible for a routine to miss its contract and yet return to its caller in a seemingly normal state. That is the worst possible way to handle an exception.
|
||||
Behind Eiffel's exception handling scheme lies the principle -- at first an apparent platitude, but violated by many existing mechanisms -- that a routine should '''either succeed or fail'''. This is in turn a consequence of Design by Contract™ principles: succeeding means being able to fulfill the contract, possibly after one or more <code>retry</code>; failure is the other case, which must always trigger an exception in the caller. Otherwise it would be possible for a routine to miss its contract and yet return to its caller in a seemingly normal state. That is the worst possible way to handle an exception.
|
||||
|
||||
Concretely, exceptions may result from the following events: <br/>
|
||||
* A routine failure ( <code> rescue </code> clause executed to the end with no <code> retry </code>), as just seen.
|
||||
* A routine failure ( <code>rescue</code> clause executed to the end with no <code>retry</code>), as just seen.
|
||||
* Assertion violation, if for a system that runs with assertion monitoring on.
|
||||
* Attempt to call a feature on a void reference: <code> x.f (...) </code>, the fundamental computational mechanism, can only work if <code> x </code> is attached to an object, and will cause an exception otherwise.
|
||||
* Attempt to call a feature on a void reference: <code>x.f (...)</code>, the fundamental computational mechanism, can only work if <code>x</code> is attached to an object, and will cause an exception otherwise.
|
||||
* Developer exception, as seen next.
|
||||
* Operating system signal:arithmetic overfolow; no memory available for a requested creation or clone -- even after garbage collection has rummaged everything to find some space. (But no C/C++-like "wrong pointer address", which cannot occur thanks to the statically typed nature of Eiffel.)
|
||||
|
||||
|
||||
It is sometimes useful, when handling exceptions in <code> rescue </code> clauses, to ascertain the exact nature of the exception that got the execution there. For this it is suffices to inherit from the Kernel Library class <code> EXCEPTIONS </code>, which provides queries such as <code> exception </code>, giving the code for the last exception, and symbolic names ( [[10 Other Mechanisms|"Constant and unique attributes", page 83]] ) for all such codes, such as <code> No_more_memory </code>. You can then process different exceptions differently by testing <code> exception </code> against various possibilities. The method strongly suggests, however, that exception handling code should remain simple; a complicated algorithm in a <code> rescue </code> clause is usually a sign that the mechanism is being misused. Class <code> EXCEPTIONS </code> also provides various facilities for fine-tuning the exception facilities, such as a procedure <code> raise </code> that will explicitly trigger a "developer exception" with a code than can then be detected and processed. Exception handling helps produce Eiffel software that is not just correct but robust, by planning for cases that should not normally arise, but might out of Murphy's law, and ensuring they do not affect the software's basic safety and simplicity.
|
||||
It is sometimes useful, when handling exceptions in <code>rescue</code> clauses, to ascertain the exact nature of the exception that got the execution there. For this it is suffices to inherit from the Kernel Library class <code>EXCEPTIONS</code>, which provides queries such as <code>exception</code>, giving the code for the last exception, and symbolic names ( [[10 Other Mechanisms|"Constant and unique attributes", page 83]] ) for all such codes, such as <code>No_more_memory</code>. You can then process different exceptions differently by testing <code>exception</code> against various possibilities. The method strongly suggests, however, that exception handling code should remain simple; a complicated algorithm in a <code>rescue</code> clause is usually a sign that the mechanism is being misused. Class <code>EXCEPTIONS</code> also provides various facilities for fine-tuning the exception facilities, such as a procedure <code>raise</code> that will explicitly trigger a "developer exception" with a code than can then be detected and processed. Exception handling helps produce Eiffel software that is not just correct but robust, by planning for cases that should not normally arise, but might out of Murphy's law, and ensuring they do not affect the software's basic safety and simplicity.
|
||||
|
||||
==Other applications of Design by Contract™==
|
||||
|
||||
|
||||
@@ -267,21 +267,29 @@ Following the principle of Uniform Access (mentioned earlier in the section ''Ob
|
||||
|
||||
In the case of a routine with arguments -- procedure or function -- the routine will be declared, in its class, as
|
||||
<code>
|
||||
feature (formal1: TYPE1; ...)
|
||||
some_feature (formal_1: TYPE_1; ...)
|
||||
do
|
||||
...
|
||||
end
|
||||
</code>
|
||||
|
||||
meaning that, at the time of each call, the value of each formal will be set to the corresponding actual ( <code>formal1</code> to <code>argument1</code> and so on).
|
||||
meaning that, at the time of each call, the value of each formal will be set to the corresponding actual (<code>formal_1</code> to <code>argument_1</code> and so on).
|
||||
|
||||
In the routine body, it is not permitted to change the value of a formal argument, although it is possible to change the value of an attached object through a procedure call such as <code> formal1.some_procedure ( ... )</code> .
|
||||
In the routine body, it is not permitted to change the value of a formal argument, although it is possible to change the value of an attached object through a procedure call such as <code>formal_1.some_procedure ( ... )</code> .
|
||||
|
||||
==Infix and prefix notation==
|
||||
|
||||
Basic types such as <code>INTEGER</code> are, as noted, full-status citizens of Eiffel's type system, and so are declared as classes (part of the Kernel Library). <code>INTEGER</code>, for example, is characterized by the features describing integer operations: plus, minus, times, division, less than, and so on.
|
||||
|
||||
With the dot notation seen so far, this would imply that simple arithmetic operations would have to be written with a syntax such as <code>i.plus (j)</code> instead of the usual <code>i + j</code>. This would be awkward. Infix and prefix features solve the problem, reconciling the object-oriented view of computation with common notational practices of mathematics. The addition function is declared in class <code>INTEGER</code> as
|
||||
With the dot notation seen so far, this would imply that simple arithmetic operations would have to be written with a syntax such as
|
||||
<code>
|
||||
i.plus (j)
|
||||
</code>
|
||||
instead of the usual
|
||||
<code>
|
||||
i + j
|
||||
</code>
|
||||
This would be awkward. Infix and prefix features solve the problem, reconciling the object-oriented view of computation with common notational practices of mathematics. The addition function is declared in class <code>INTEGER</code> as
|
||||
<code>
|
||||
infix "+" (other: INTEGER): INTEGER
|
||||
do
|
||||
@@ -289,11 +297,14 @@ infix "+" (other: INTEGER): INTEGER
|
||||
end
|
||||
</code>
|
||||
|
||||
Such a feature has all the properties and prerogatives of a normal "identifier" feature, except for the form of the calls, which is infix, as in <code>i + j</code> , rather than using dot notation. An infix feature must be a function, and take exactly one argument. Similarly, a function can be declared as <code>prefix "-" </code>, with no argument, permitting calls of the form <code> -3 </code> rather than <code>(3).negated</code> .
|
||||
Such a feature has all the properties and prerogatives of a normal "identifier" feature, except for the form of the calls, which is infix, as in <code>i + j</code> , rather than using dot notation. An infix feature must be a function, and take exactly one argument. Similarly, a function can be declared as <code>prefix "-" </code>, with no argument, permitting calls of the form <code>-3</code> rather than <code>(3).negated</code> .
|
||||
|
||||
Predefined library classes covering basic types such as <code>INTEGER</code>, <code>CHARACTER</code>, <code>BOOLEAN</code>, <code>REAL</code>, <code>DOUBLE</code> are known to the Eiffel compiler, so that a call of the form <code>j + i</code>, although conceptually equivalent to a routine call, can be processed just as efficiently as the corresponding arithmetic expression in an ordinary programming language. This brings the best of both worlds: conceptual simplicity, enabling Eiffel developers, when they want to, to think of integers and the like as objects; and efficiency as good as in lower-level approaches.
|
||||
|
||||
Infix and prefix features are available to any class, not just the basic types' predefined classes. For example a graphics class could use the name <code>infix "|-|"</code> for a function computing the distance between two points, to be used in expressions such as <code>point1 |-| point2</code> .
|
||||
Infix and prefix features are available to any class, not just the basic types' predefined classes. For example a graphics class could use the name <code>infix "|-|"</code> for a function computing the distance between two points, to be used in expressions such as
|
||||
<code>
|
||||
point1 |-| point2
|
||||
</code>
|
||||
|
||||
==Type declaration==
|
||||
|
||||
@@ -412,7 +423,7 @@ To copy an object, use
|
||||
</code>
|
||||
which assumes that both <code>x</code> and <code>y</code> are non-void, and copies the contents of <code>y</code>'s attached object onto those of <code>x</code>'s. For expanded entities the effect is the same as that the of the assignment <code>x := y</code>.
|
||||
|
||||
An operation performing similar duty to the <code>copy</code> is <code>twin</code> . The assignment
|
||||
An operation performing similar duty to <code>copy</code> is <code>twin</code> . The assignment
|
||||
<code>
|
||||
x := y.twin
|
||||
</code>
|
||||
@@ -427,7 +438,6 @@ So, assuming both entities of reference types and <code>y</code> not void, the a
|
||||
|
||||
|
||||
To determine whether two values are equal, use the expression:
|
||||
|
||||
<code>
|
||||
x = y
|
||||
</code>
|
||||
@@ -464,7 +474,7 @@ and test whether it is void through:
|
||||
|
||||
Note that the assignment, <code>:=</code> , and the equality operators, <code>=</code>, <code>~</code>, <code>/~</code>, and <code>/=</code> , are language constructions, whereas <code>copy</code>, <code>twin</code>, <code>is_equal</code>, and <code>equal</code> are '''library features''' coming from class <code>ANY</code> .
|
||||
|
||||
<code>Void</code> is a language keyword with built-in functionality, but it is not harmful to think of <code>Void</code> as another feature declared in <code> ANY </code>, but with type of <code>NONE</code>, the "bottom" type.
|
||||
<code>Void</code> is a language keyword with built-in characteristics, but it is not harmful to imagine <code>Void</code> as another feature declared in class <code>ANY</code>, with type of <code>NONE</code>, the "bottom" type. This convenience allows any assignment of the for <code>x := Void</code> to be valid without any making exceptions to the type rules, regardless of the type of <code>x</code> .
|
||||
|
||||
Using the redefinition mechanisms to be seen in the discussion of inheritance, a class can redefine <code>copy</code> and <code>is_equal</code> to cover specific notions of copy and equality. The assertions will ensure that the two remain compatible: after <code>x.copy (y)</code> , the property <code>x .is_equal (y)</code> must always be true. The effect of <code>twin</code> will automatically follow a redefinition of <code>copy</code>, and <code>equal</code> will follow <code>is_equal</code>.
|
||||
|
||||
|
||||
@@ -22,7 +22,7 @@ Within the class text, feature declarations can freely use <code>G</code> even t
|
||||
first: G
|
||||
-- Value of first list item
|
||||
|
||||
extend (val: G) is
|
||||
extend (val: G)
|
||||
-- Add a new item of value val at end of list
|
||||
...
|
||||
</code>
|
||||
@@ -45,23 +45,23 @@ Genericity reconciles extendibility and reusability with the static type checkin
|
||||
|
||||
==Arrays==
|
||||
|
||||
An example of generic class from the Kernel Library is <code>ARRAY</code> <code>[</code> <code>G</code> <code>]</code>, which describes direct-access arrays. Features include:
|
||||
* <code>put</code> to replace an element's value, as in <code>my_array</code>. <code>put</code> <code>(</code> <code>val</code>, <code>25</code> <code>)</code> which replaces by <code>val</code> the value of the array entry at index 25.
|
||||
* <code>item</code> to access an entry, as in <code>my_array</code>. <code>item</code> <code>(</code> <code>25</code> <code>)</code> yielding the entry at index 25. A synonym is <code>infix</code> <code>"@"</code>, so that you may also write more tersely, for the same result, <code>my_array</code> <code>@</code> <code>25</code>.
|
||||
An example of generic class from the Kernel Library is <code>ARRAY</code> <code>[G]</code>, which describes direct-access arrays. Features include:
|
||||
* <code>put</code> to replace an element's value, as in <code>my_array.put (val, 25)</code> which replaces by <code>val</code> the value of the array entry at index 25.
|
||||
* <code>item</code> to access an entry, as in <code>my_array.item (25)</code> yielding the entry at index 25. A synonym is <code>infix</code> <code>"@"</code>, so that you may also write more tersely, for the same result, <code>my_array</code> <code>@</code> <code>25</code> .
|
||||
* <code>lower</code>, <code>upper</code> and <code>count</code>: queries yielding the bounds and the number of entries.
|
||||
* The creation procedure <code>make</code>, as in <code>create</code> <code>my_array</code>. <code>make</code> <code>( 1, 50 )</code> which creates an array with the given index bounds. It is also possible to resize an array through <code>resize</code>, retaining the old elements. In general, the Eiffel method abhors built-in limits, favoring instead structures that resize themselves when needed, either from explicit client request or automatically.
|
||||
* The creation procedure <code>make</code>, as in <code>create my_array.make (1, 50)</code> which creates an array with the given index bounds. It is also possible to resize an array through <code>resize</code>, retaining the old elements. In general, the Eiffel method abhors built-in limits, favoring instead structures that resize themselves when needed, either from explicit client request or automatically.
|
||||
|
||||
The comment made about <code>INTEGER</code> and other basic classes applies to <code>ARRAY</code> too: Eiffel compilers know about this class, and will be able to process expressions of the form <code>my_array</code>. <code>put</code> <code>(</code> <code>val</code>, <code>25</code> <code>)</code> and <code>my_array</code> <code>@</code> <code>25</code> in essentially the same way as a C or Fortran array access -- <code>my_array</code> <code>[</code> <code>25</code> <code>]</code> in C. But it is consistent and practical to let developers treat <code>ARRAY</code> as a class and arrays as objects; many library classes in EiffelBase, for example, inherit from <code>ARRAY</code>. Once again the idea is to get the best of both worlds: the convenience and uniformity of the object-oriented way of thinking; and the efficiency of traditional approaches.
|
||||
The comment made about <code>INTEGER</code> and other basic classes applies to <code>ARRAY</code> too: Eiffel compilers know about this class, and will be able to process expressions of the form <code>my_array.put (val, 25)</code> and <code>my_array</code> <code>@</code> <code>25</code> in essentially the same way as a C or Fortran array access -- <code>my_array</code> <code>[25]</code> in C. But it is consistent and practical to let developers treat <code>ARRAY</code> as a class and arrays as objects; many library classes in EiffelBase, for example, inherit from <code>ARRAY</code>. Once again the idea is to get the best of both worlds: the convenience and uniformity of the object-oriented way of thinking; and the efficiency of traditional approaches.
|
||||
|
||||
A similar technique applies to another Kernel Library class, that one not generic: <code>STRING</code>, describing character strings with a rich set of string manipulation features.
|
||||
|
||||
==Generic derivation==
|
||||
|
||||
The introduction of genericity brings up a small difference between classes and types. A generic class <code>C</code> is not directly a type since you cannot declare an entity as being of type <code>C</code>: you must use some actual generic parameter <code>T</code> -- itself a type. <code>C</code> <code>[</code> <code>T</code> <code>]</code> is indeed a type, but class <code>C</code> by itself is only a type template.
|
||||
The introduction of genericity brings up a small difference between classes and types. A generic class <code>C</code> is not directly a type since you cannot declare an entity as being of type <code>C</code>: you must use some actual generic parameter <code>T</code> -- itself a type. <code>C</code> <code>[T]</code> is indeed a type, but class <code>C</code> by itself is only a type template.
|
||||
|
||||
The process of obtaining a type <code>C</code> <code>[</code> <code>T</code> <code>]</code> from a general class <code>C</code> is known as a '''generic derivation'''; <code>C</code> <code>[</code> <code>T</code> <code>]</code> is a '''generically derived type'''. Type <code>T</code> itself is, recursively, either a non-generic class or again a generically derived type <code>D</code> <code>[</code> <code>U</code> <code>]</code> for some <code>D</code> and <code>U</code>, as in <code>LIST</code> <code>[</code> <code>ARRAY</code> <code>[</code> <code>INTEGER</code> <code>]]</code>.)
|
||||
The process of obtaining a type <code>C</code> <code>[T]</code> from a general class <code>C</code> is known as a '''generic derivation'''; <code>C</code> <code>[T]</code> is a '''generically derived type'''. Type <code>T</code> itself is, recursively, either a non-generic class or again a generically derived type <code>D</code> <code>[U]</code> for some <code>D</code> and <code>U</code>, as in <code>LIST</code> <code>[ARRAY [INTEGER]]</code>.)
|
||||
|
||||
It remains true, however, that every type is based on a class. The base class of a generically derived type <code>C</code> <code>[</code> <code>T</code> <code>]</code> is <code>C</code>.
|
||||
It remains true, however, that every type is based on a class. The base class of a generically derived type <code>C</code> <code>[T]</code> is <code>C</code>.
|
||||
|
||||
|
||||
|
||||
|
||||
Reference in New Issue
Block a user