Previous | Table of Contents | Next |
Because it is impossible to check simply that an assertion is weaker or stronger than another, the language rule relies on new variants of the assertion constructs: require else and ensure then, relying on the mathematical property that, for any assertions p and q, p implies (p or q), and (p and q) implies p. For a precondition, using require else with a new assertion performs an or, which can only weaken the original; for a postcondition, ensure then performs an and, which can only strengthen the original. Hence, the rule:
Assertion redeclaration rule:
In the redeclared version of a routine, it is not permitted to use a require or ensure clause. Instead, you may
- Use a clause introduced by require else, to be or-ed with the original precondition.
- Use a clause introduced by ensure then, to be and-ed with the original postcondition.
In the absence of such a clause, the original assertion is retained.
The last caseretaining the originalis frequent, but by no means universal.
The assertion redeclaration rule applies to redeclarations. This terms covers not just redefinition but also effecting (the implementation, by a class, of a feature that it inherits deferred). The rulesnot just for assertions but also, as reviewed below, for typingare indeed the same in both cases. Without the assertion redeclaration rule, assertions on deferred features, such as those on extend, count, and forth in section 9.9.5, would be almost uselesswishful thinking; the rule makes them binding on all effectings in descendants.
From the assertion redeclaration rule follows an interesting technique: abstract preconditions. What needs to be weakened for a precondition (or strengthened for a postcondition) is not the assertions concrete semantics but its abstract specification as seen by the client. A descendant can change the implementation of that specification as it pleases, even to the effect of strengthening the concrete precondition, as long as the abstract form is kept or weakened. The precondition of procedure extend in the deferred class LIST provided an example. We wrote the routine (section 9.9.5) as
extend (x: G) is -- Add x at end of list. require space_available: not full deferred ensure one_more: count = old count + 1 end
The precondition expresses that it is only possible to add an item to a list if the representation is not full. We may well considerin line with the Eiffel principle that whenever possible structures should be of unbounded capacitythat LIST should by default make full always return false:
full: BOOLEAN is -- Is representation full? -- (Default: no) do Result := False end
Now a class BOUNDED_LIST that implements bounded-size lists (inheriting, like the earlier ARRAYED_LIST, from both LIST and ARRAY) may redefine full:
full: BOOLEAN is -- Is representation full? -- (Answer: if and only if number of items is capacity) do Result := (count = capacity) end
Procedure extend remains applicable as before; any client that used it properly with LIST can rely polymorphically on the FIXED_LIST implementation. The abstract precondition of extend has not changed, even though the concrete implementation of that precondition has in fact been strengthened.
Note that a class such as BOUNDED_LIST, the likes of which indeed appear in EiffelBase, is not a violation of the Eiffel advice to stay away from fixed-size structures. The corresponding structures are bounded, but the bounds are changeable. Although extend requires not full, another feature, called force by convention, is available to work in all cases, resizing (and possibly reallocating) the structure if necessary. Even arrays in Eiffel are not fixed-size and have a procedure force with no precondition, accepting any index position.
The assertion redeclaration rule, together with the invariant accumulation rule, provides the right methodological perspective for understanding inheritance and the associated mechanisms. Defining a class as inheriting from another is a strong commitment; it means inheriting not only the features but also the logical constraints. Redeclaring a routine is a committing decision: It means that you are providing a new implementation (or, for an effecting, a first implementation) of a previously defined semantics, as expressed by the original contract. Usually you have a wide margin for choosing your implementation because the contract only defines a range of possible behaviors (rather than just one behavior), but you must remain within that range. Otherwise, you would be perverting the goals of redeclaration, using this mechanism as a sort of late-stage hacking to override bugs in ancestor classes.
Previous | Table of Contents | Next |