or preferably: "attached assertions"
"Design By Contract" is a trademark of Interactive Software Engineering referring to special expressive means of the Eiffel language. See, e.g., the equally named section in the Eiffel Tutorial of ISE: In Eiffel you can specify pre- and postconditions for methods and invariants for classes, and also some other kinds of assertions.
Lava provides preconditions, postconditions, invariants, and assert statements, too, with a number of differences, as compared with Eiffel, that should be noted (see below).
We have used the term "design by contract" in the title because it is well-known in professional circles and because of some basic similarities of the Lava approach with that of Eiffel. Actually we don't like the term since "design by contract" suggests the idea of a precise contract between customer and programmer, in the sense of comprehensive necessary and sufficient conditions for the correctness of method implementations which completely specify
what the caller of a method should make sure on entry to the method (precondition) and
what the programmer of the method should guarantee on exit from the method (postcondition),
while a class invariant is a condition that should be true on every entry to and exit from a (public) method of the class.
Such a comprehensive, complete, formal contract would require the expressive means of a specialized specification language, however, and such expressive means are neither provided by Eiffel, nor by Lava:
In place of "design by contract" we prefer to speak of attached assertions (pre- and postconditions are attached to methods, invariants to classes) and of assertion checking. The term "attached assertions" emphasizes that such an assertion isn't embedded within normal executable code but attached to the declarations/implementations of methods and classes; their execution is triggered by the run time system on specific occasions (entry/exit to/from methods). Checking of attached assertions may also be switched off on demand.
The purpose of such assertions is
to provide additional documentation and explanations
on the semantics of methods and classes and
on implementation restrictions and limitations that the user of these classes and methods has to observe.
to serve as a debugging aid: the assertions provide additional redundant information on methods and classes that (hopefully) will enable early detection of programming errors before they end up in obscure crashes.
Lava pre/postconditions and invariants are checked at run time according to the following rules:
Preconditions are checked immediately before entry to the corresponding method to which they are attached. The method body is skipped if an exception occurs in the precondition.
Postconditions are checked immediately after the body of the method has been left (if no exception has been thrown by the method body.
Invariants (including all invariants "inherited" by a class from its direct and indirect base classes) are checked on object creation when the new object leaves the new expression, and on entry/exit to/from every public non-read-only method; for read-only methods only on entry (cf. subsection D) of the next section).
Assertion checking is turned off within assertions to avoid infinite recursions which otherwise could easily occur. (E.g., assertions attached to a method m1 of some class would frequently make use of a method m2 of that class, while the assertions attached to m2 may refer to m1 again, or similarly.)
In addition to the actual checking of pre/postconditions Lava checks also the consistency of these assertions with those of overridden methods: See subsection C) of the next section.
In Eiffel, assertions are expressed by Boolean expressions, while
Lava has considerably more general expressive means, including all kinds of statements, like assignment, branching, and function call statements (with more than one output), comparison statements, and quantifiers.
The only restriction is that a Lava assertion must have the read-only property, i.e, it must not modify pre-existing objects (= objects that existed already before starting the evaluation of the assertion). The Lava programming environment LavaPE makes this sure already at programming time.
You should not in this context that executable Lava statements can be viewed as logical statements. Execution of a statement means verification and yields the result true or false (if no exception is thrown). As a consequence, where other programming languages would use Boolean expressions, for instance in if-conditions, Lava uses quite normal ("read-only" or, as in if-conditions, even "assignment-free") statements.
Note also that comparisons
<expression> <comparison-operator> <expression>
are statements in Lava, not Boolean expressions.
Like Eiffel, Lava provides an "old <expression>" which allows you to refer to the original value of an expression (on method entry) within postconditions and method bodies. The Lava "old" expression has a more satisfactory semantics, however (see below).
In Lava, declaration and implementation of methods and classes are strictly separated; as an obvious consequence, assertions can be attached to both.
This is in fact highly desirable, since it allows us to adequately express not only "logical" assertions which characterize the actual logic and semantics of classes and methods, but also purely implementation-related assertions which describe restrictions and limitations of the respective implementation.
For instance, if you implement a "table" class on the basis of an array of fixed length then you have an implementation restriction concerning the capacity of the table. This may be perfectly acceptable for the intended application, but it is by no means an inherent semantic restriction of a "table" class. In this case you could attach a quite natural "capacity check" precondition to the implementations of all "table" methods that add a new element to the table.
Moreover, it is desirable to distinguish this kind of "implementation-related" assertions from "semantical assertions" since the "hierarchy correctness checks" of the next section are justified only for the latter and don't make sense for the former.
These are also known as "hierarchy correctness checks" in the context of "Behavioral Subtyping"; cf., e.g., [1] and [2] below. They make sure that the behavior of derived classes, taking pre- and postconditions into account, should comply with the behavior of base classes. Here are the two basic principles that govern these consistency checks:
If we have a class C1, and a class C2 derived from C1, and a (public) method m in C1 which is overridden in C2, and if m has a precondition pr1 in C1and pr2 in C2, and if a concrete invocation of the method (with a call object of class C2) would be admissible according to pr1 then it should also be admissible according to pr2. In other words: If pr1 evaluates to
true in the concrete case then pr2 should also evaluate to
true. This applies also if pr1 is absent (= always
true): pr2 must also be always true (for instance absent). (If pr2 is absent then pr1 trivially implies pr2.) Roughly spoken:
The precondition of an overriding method should be equivalent to or at most weaker than that of a corresponding overridden method.
And for postconditions po1 and po2: If a concrete invocation of the method (with a call object of class C2) is admissible according to preconditions pr1 (and therefore, because of 1. above also pr2) and consequently ensures the validity of postcondition po2 then it should also ensure the validity of postcondition po1. In other words: If pr1, pr2 and po2 evaluate to true in the concrete case then po1 should also evaluate to
true. Roughly spoken:
The postcondition of an overriding method should be equivalent to or at most stronger than that of a corresponding overridden method.
Note 1: Since Lava supports multiple inheritance a method may override several methods (of several base classes). Then the two consistency rules apply to all these overridden methods.
Note 2: Lava supports virtual types (= parameter types of classes and packages) and substitutable types. If a class derivation is induced by the specialization of a virtual type then it may happen that an overridden method cannot be invoked with an object of the derived class. In this case the assertion consistency rules do not apply, since the pre/postconditions of the overridden method generally cannot be evaluated, too.
In contrast to Lava, Eiffel does not check the consistency of preconditions of overridden and overriding methods but enforces consistency by automatically connecting all these preconditions by a logical OR conjunction. Newer research articles (like [1] and [2] below) call this approach into question and recommend a consistency checking approach since automatic ORing may mask a real inconsistency and fail to report it. It may then falsely come to the surface as a postcondition violation which is caused by the fact that the ORed preconditions are too weak to actually ensure the intended postcondition.
The evaluation of an assertion should not change the referenced objects or any other "pre-existing" objects, i.e., objects that existed already before the evaluation started. In Lava this is guaranteed owing to the read-only property of assertions, which can be checked already at programming time in Lava.
Another nice side effect of the fact that Lava can guarantee the read-only property of methods: Lava does not have to to check invariants after read-only methods since the latter cannot change any objects that existed already on entry to the method.
Like Eiffel, Lava provides an "old <expression>" which allows you to refer to the original value of an expression (on method entry) within postconditions and method bodies. The implementation of old requires to evaluate the <expression> on method entry and to store a copy of the resulting object for later reference. (The original result object might be modified before it is actually referenced by the respective "old <expression>".)
Naturally this raises the question: What is a copy of an object? The copy notion calls for a precise answer to the question: What belongs to the object? Fortunately, concerning the attributes (or member objects) of an object, Lava provides a clear distinction between constituents and acquaintances. The former (and also constituents of constituents, etc.) belong to the object, while acquaintances (also of nested constituents) just point to independent objects.
Without such a distinction you can provide only a more or less undifferentiated and arbitrary semantics of "old <expression>" which won't reflect the application needs in many cases.
The ISE Eiffel Tutorial states on page 41:
"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 require n> 0, where n is a secret attribute-the supplier would be making demands that a good-faith client cannot possibly check for."
In Lava we don't need such special rules since attached assertions in class interfaces can only reference class features that are declared in that class interface. ("Private" features, declared in class implementations, can be referenced only from within that implementation and are invisible to the "outside world", including to the assertions in the corresponding interface.)
[1] R.B. Findler, M. Felleisen: Contract Soundness for Object-Oriented Languages, OOPSLA 2001.
[2] R.B. Findler, M. Latendresse, M. Felleisen: Behavioral Contracts and Behavioral Subtyping, FSE 2001.