Keywords: inheritance, class invariants, require else, ensure then.
Inheritance of assertions guarantees that the behavior of a class is compatible with that of its ancestors. For example, a class should not assume a state that would be invalid for any of its predecessors; therefore it must satisfy all their invariants. Similarly, a class must be able to perform (at least) all the functions of its ancestors; therefore, the redefinition of a routine may only weaken the precondition and strengthen the post-condition. The pre- and post-conditions for a routine redefinition are designated by the keywords require else and ensure then respectively. The precondition for a redefined routine is equivalent to the new precondition or else the precondition from the original routine, while the post-condition is equivalent to the new post-condition and then the original.
Pre- and post-conditions and class invariants allow us to describe many properties of software components. We can use these assertions to write software contracts which may be monitored at run-time to ensure compliance. However, we need to realize that these tools are embedded in a language which supports inheritance; therefore, classes can redefine routines inherited from their parents. To complete our understanding of assertions and their use, we must now examine how the tools presented so far interact with inheritance.
The inheritance mechanisms provided by Eiffel are powerful, and if used correctly can lead to smaller, more elegant systems consisting of easily reusable components. However, these mechanisms can also lead to chaos if misused. If redefinition and dynamic binding are allowed to arbitrarily change the behavior of operations, clients will be unable to depend on stable, predictable outcomes. Assertions can provide an answer to this problem. Briefly, in Eiffel descendants inherit the class invariants of their parents, and any redefinition of a routine must satisfy the original pre- and post-conditions; therefore, if client code relies only on properties specified using assertions, all descendants are guaranteed to perform all functions required of their ancestors.
We can extend our contracting metaphor to view the inheritance of assertions as programming by sub-contract. In the real world, a general contractor may hire any number of others to perform parts of the original job; however, these sub-contractors must perform the work up to the standards required in the overall contract, and must do it cheaply enough so that the general contractor can complete the entire job for the agreed upon price. In Eiffel, descendants can only do more, cheaper than their ancestors. Specifically, any redefinition of a routine may only change the post-condition by making it stronger (more difficult to satisfy); therefore, all descendants are guaranteed to perform (at least) all the functions of their ancestors. Similarly, any redefinition may only change the precondition by making it weaker (easier to satisfy); therefore, all descendants are guaranteed to perform in (at least) all cases their ancestors would accept.
In Eiffel, a class inherits the invariants of all its ancestors, so each instance of the descendent class must satisfy the invariant of each ancestor class. For example, if the class HOUSE_CAT is a descendent of both CAT and PET, and CAT is a descendant of ANIMAL, then any instance of HOUSE_CAT must satisfy the class invariants of both CAT, PET and ANIMAL. In other words, the invariant for HOUSE_CAT consists of its own invariant "and"ed with the invariants of all its ancestors. If class invariants are being monitored at run-time, then the invariants of all the ancestors of a class will be evaluated before the invariant of the class itself. For example, if class invariants are being checked, then the invariants for CAT, PET and ANIMAL will all be evaluated before the invariant for HOUSE_CAT.
As a more concrete example, let us consider the problem of maintaining an ordered list. An ordered list is simply a list in which every element is greater than or equal to all those preceding it; in other words, the first element is the list is the smallest, the second is the next to smallest, and so on. We can use the LIST class described previously to maintain an ordered list by defining a descendant class with an appropriate invariant. The first thing we must do is define the BOOLEAN function ordered, which returns true if and only if the elements of the list have the correct relationship. The function is defined on any list, so it has no precondition (in other words, it has a precondition of true). The post-condition requires that if the function returns false then the last two items examined were in the incorrect order.
The routine consists of a single loop. Result is initialized to true because an empty list is always ordered. Each pair of elements in the list is compared starting at the front of the list and continuing until the end is reached or the result is known to be false. When a pair of elements is compared, the Result is set to false if they are out of order.
ordered: BOOLEAN is
local k: INTEGER
do
from
Result := true
k := count
until
k < 2 or not Result
loop
k := k - 1
if elements.item (k - 1) < elements.item (k)
thenResult := false
end
end
ensure
not Result
implies elements.item (k - 1) < elements.item (k)
end -- ordered
We can now define the class ORDERED_LIST as a descendant of LIST that exports the same features. The major difference between the two is that ORDERED_LIST has a class invariant requiring that the items be ordered both before and after each external call to any routine. Another difference is that the elements in an ORDERED_LIST must belong to a descendant of the kernel library class COMPARABLE; this guarantees that the necessary comparison operators are defined. An ORDERED_LIST must be able to perform all the functions of a LIST from the client's point of view. While most of the operations will be identical, the insert routine must be modified to maintain the ordering relation when a new element is added.
class ORDERED_LIST [T -> COMPARABLE]
inherit
LIST [T]
redefine insert
end
feature {ANY}
insert (elem: T) is
-- insert elem, maintaining sorted order
• • •
ordered: BOOLEAN is
• • •
invariant
ordered: ordered
end -- class ORDERED_LIST
In Eiffel, the inheritance of pre- and post-conditions supports programming by sub-contract; any redefinition of a routine must satisfy a precondition that is at least as easy to satisfy as the original, and a post-conditions that is a least as demanding as the original. In other words, a sub-contractor may weaken the precondition and strengthen the post-condition, but not vice versa.
Specifically, if pre- and post-conditions are present in the redefined routine they are designated with the keywords require else and ensure then respectively.
routine_name (<arguments>) is
require else
new_precondition
• • •
ensure then
new_post-condition
end -- routine_name
The new pre- and post-conditions are evaluated before the originals. In other words, the above assertions are equivalent to the following, where the original pre- and post-conditions are from the definition of the routine in the parent class. The default new precondition is false, and the default new post-condition is true.
routine_name (<arguments>) is
require
new_precondition or else original-precondition
• • •
ensure
new_post-condition and then original-precondition
end -- routine_name
If pre- and post-conditions are being monitored at run time, then the new precondition is evaluated at the beginning of each call to the routine. If it is true then execution continues with the body of the routine. If the new precondition is false then the original precondition is evaluated. If the original precondition is also false then an exception is raised and the system terminates with an appropriate message. If the original precondition is true then execution continues with the routine body. After execution of the routine body completes, the new post-condition is evaluated. If it is false then an exception is raised and the system terminates with an appropriate message. If the new post-condition is true, then the original post-condition is evaluated. If it is true, then every thing is as it should be and the call completes normally. If it is false then an exception is raised and the system terminates with an appropriate message.
As an illustration, consider the insert procedure for the ORDERED_LIST class. The original precondition for insert required that the list was not full, and the post-condition ensured that the list was not empty, that count was increased by one, and that elements and count were the only features changed by the operation.
insert (elem: T) is
-- put an element into the list
require
not_full: not full
do
• • •
ensure
not_empty: not empty;
count_increased: count = old count + 1;
no_extra_changes: strip (elements, count).is_equal
old strip (elements, count)
end -- insert
In ORDERED_LIST, the class invariant requires that the list be ordered at the beginning of insert; therefore the precondition need not be changed, and so none appears in the redefined routine. While the original post-condition for insert is also acceptable, we will strengthen it by requiring that elem be a member of the list when the procedure terminates.
insert (elem: T) is
-- put an element into the list
do
• • •
ensure then
elem_member: member (elem)
end -- insert
The pre- and post-conditions for the redefinition of insert are equivalent to the following. Since there is no new precondition, the original is used unchanged, while the new post-condition is "and"ed on to the beginning of the original. Notice that we save considerable duplication by inheriting the pre- and post-conditions for the insert routine in the LIST class, rather than re-writing them in the pre- and post-conditions for the new routine explicitly.
insert (elem: T) is
-- put an element into the list
require
not_full: not full
do
• • •
ensure
elem_member: member (elem);
not_empty: not empty;
count_increased: count = old count + 1;
no_extra_changes:strip (elements, count).is_equal
old strip (elements, count)
&nbs