Eiffel and Design by Contract, part 2

The is a continuation of Bertrand Meyer’s first LASER talk.

Command-Query separation is an important principle of Eiffel. So instead of getint(), Eiffel uses io.read_integer and io.last_integer(). A separation of a procedure that does something and a method that returns something. The basic idea behind this is “asking a question should not change the answer”. This limits the possibilities though, since meta questions like “how many times have I asked this question?” may not be asked. Simon Peyton Jones asks whether this leads to many occurrences of a combination of a side-effecting procedure followed by a method. This is an interesting question and Bertrand agrees this is a common pattern. We should mine some Eiffel repositories to find out.

An other design principle of Eiffel is the compatibility principle: Traditional notations should be supported with OO semantics, aka ‘we shouldn’t harrass developers with annying complex operations’. So although the correct way to call is a.plus(b), Eiffel still supports a + b for convenience. This is implemented with an ‘alias’ operation. This alias can also be applied to “[]” to access array elements.

Assignments to fields of classes are strictly not allowed (because of the principle of information hiding), however x.f = 25 is accepted as abbreviation for x.setf(25), but this has to be explicitly defined, using an ‘assign’ command: f: real assign setf. These two options are a way of combining the pure ideas of Eiffel with the normal operations people are used to. While the flexibility of this is nice, it does allow for very crazy syntax like a+b := c as an abbreviation for (for instance) a.f(b,c). Even Bertrand agrees, but he states that there are “many ways in which one can write a bad Eiffel program”.

Design by Contract

The idea of DbC is: Every software element should be characterized by a precise specification. Bertrand first submitted a paper on this in 1987, but it was under review for 6(!) years.

Everything you program has a goal, in DbC this goal is made explicit using a contract. Bertrand states this goal should be in the code, and not just in the head of the developer. If it is just in the head of the developer, it might lead to errors like the Ariane-5 disaster. There the assumption was documented, but not tested or checked.

DbC supports for class invariant, require and ensure commands, that you can use to express what assertions should hold for the implementation. Require is a precondition and require is a postcondition, in which you can use ‘old’ on a variable to compare the version of the variable before the method was executed. So a postcondition is an assertion on two objects, the old and new version of the variable.

More Eiffel tomorrow!