Design by Contract in Eiffel, part 3

The third day of LASER starts with the third lecture by Bertrand Meyer on DbC In Eiffel. No clue what that is? I kindly refer you to Lecture 1 and Lecture 2 or Wikipedia.

The class invariant

Is a consistency constraints has to be satisfied ‘always’, well that is, before starting a procedure and when the procedure is finished. While in a procedure, it might be violated, since the program is in a state of computation. As Bertrand explains it, when a presenter gives a lecture, it is important that the audience understands everything when starting a new slide. While explaining the slide the audience might struggle, but upon leaving it, everybody should be back on board. Funny analogy.

The benefit of contracts

Bertrand argues that a class invariant is also a way of expressing the functionality of a class, for instance balance = depostis.total – withdrawals.total expresses the relationship between withdrawals and deposits. In addition to documentation purposes, the biggest benefit of contracts is, obviously, its help for writing correct software: analysis, design and even proofs about the software.

Contracts and assurance

Using the contracts, we can pinpoint easily what goes wrong, when something goes wrong. Suppose we have a program like this:

{P} A {Q}

Now, the type of the violation helps us understand the problem as follows:

Violation of P: bug in the client
Violation of Q: bug in the supplier
Invariant violation: bug in the supplier

In Eiffel you can set the way contracts are checked per class, like nothing, only preconditions, or everything. Bertrand stressed the importance of DbC by citing

“I believe that the use of Eiffel-like module contracts is the most important non-practice in software today.” – Tom DeMarco

AutoTest

Where DbC has existed in Eiffel for its entire lifespan, AutoTest is a relative new feature (past 5,6 years). AutoTest selects classes and executes their methods is a sort of random way(tries dangerous values like 0, -1, manual tests can be added if needed). If there is a precondition violation, the method is skipped, but if there is a postcondition or invariant violation, a bug is detected.

Automated documentation generation

From an Eiffel program, we can automatically extract all assertions in a sort of readable way, to serve as documentation. This documentation will always be up to date and does not have to be written by hand.

The contract view is created by removing implementation details and ‘secret’ elements (private). There is however a problem is this, since preconditions need to be visible in order for users to be able to call them correctly.