Design by Contract in Eiffel, part 4

Time for the 4th lecture on DbC (See: Lecture 1 and Lecture 2 and Lecture 3 or Wikipedia)

Bertrand starts off with stating that people often criticize Eiffel by saying that “Real programmers don’t write assertions”

Bertrand thinks this is non true. I agree, even many (non-programmer) spreadsheet builders often use a form of assertions. However, developers usually write them after the fact. Before is better, since then the problem is fresh in your head. And, by doing if beforehand, you get all the benefits of DbC. And this does not need to be Coq-like statements, referring to Simon’s joke:

“Assertions in Eiffel are ordinary stuff for ordinary people.”

Contract and inheritance

When redeclaring (overriding or effecting) a new routing, assertions are kept by default. The new precondition may be weaker and the postcondition may be stronger, this is defined with ‘require else’ and ‘ensure then’. This prohibits a user to implement different too behavior when redeclaring.

Exception handling

In its basis exception handling in Eiffel does not differ that much from other languages, but in addition to exceptions, there is the concept of ‘failure’ which means that a method is unable to fulfill its contract. Two ways to react on an exception (“not doing this is bad for your reputation as an object” – Bertrand) Organized panic(Failure) or Try Again. The options are grouped in the rescue clause, where a retry can be executed, for instance up to a number of tries. If you want to know more, try (and possibly retry 🙂 Bertrand’s Disciplined Exceptions paper.

The assertion language

Assertions in Eiffel use boolean expressions in the programming language, plus old in postconditions representing the original state. Benefits of expressing the assertions in the language itself (as opposed to a formal language, like Z) makes it possible to do static checking for proofs. However, downside is that there is no first- or higher-order predicate calculus. You can use queries in assertions, however, there may not be side effects.

To overcome the limitations, the Eiffel Model Library (MML) was introduced, mainly the work of Nadia Polikarpova.  This is a library with classes that correspond to mathematical concepts, like set, function, total_function and the such. These classes do not have an implementation, but have contracts that express their behavior. They are not imperative classes, but are more like functional objects. For example, the SEQUENCE class does not have a method ‘extend’ (which is imperative) but a predicate ‘extended’.

By using the MML, it is possible to translate first-order predicates into standard Eiffel contracts. Although I do not have the feeling that I grasp all details of MML, I really like the approach and of using design by contract to implement first-order logic that can be subsequently used (and checked) in Eiffel itself.