Assertion Settings

Author: Matthias Konrad

Introduction

The Eiffel Language specifies several assertion types:

• Preconditions
• Postconditions
• Invariants
• Loop variants
• Checks

In theory these assertions should be checked all the time. In practice, especially when working with huge systems, this is not possible. (Quite often it is not even possible during the testing phase of the system.) It is thus nessecary to decide which assertions should be tested.

It is not sufficient to just enable or disable a certain assertion kind for the whole system. Large systems are composed of smaller parts and reused components (like the base library). These are typically tested independently (unit level testing). It should thus be possible to disable assertion testing on the tested parts and enable it on the other parts.

EiffelStudio lets the user decide which assertion kinds are checked for every class.

Proposal for a property: Supplier_preconditions

At the moment, when the user mistrusts a class, he has to enable precondition checking both for the class itself and all the supplier classes. This has two drawbacks:

• It is tedious to find the suppliers and change their configuration. So in practice users just enable precondition checking for the whole system. (Which makes the next drawback even worse.)
• There are more precondition checks at runtime than necessary.

It would thus be nice if one could specify for a class, that all the preconditions of its called features are checked. Not allways, but only when they are called by this class. This option would typically be enabled on all the untested (and therefore untrusted) classes and disabled on the others for performance reasons.

Proposal for a property: Supplier_invariants

Since invariants may depend on side-effects, they have to be tested both on entry and on exit of every qualified call. The on entry test can be seen as an additional precondition and the on exit test as a postcondition. A class that is properly tested will never invalidate its invariant itself, but an other class (an untested one) might do it. Since untested classes may, through side-effects invalidate the invariants of tested classes, the invariants

A user can specify whether the assertions of a given kind are checked on a per class basis.

When the user specifies the assertions for a class he expresses a certain level of trust or mistrust towards it. When he enables invariant checking for a class he is not sure wether the specified invariants really hold, so they need to be checked. The same thing is true for loop variants, postconditions and checks. Whereas for preconditions there is different. When precondition checking is enabled the user mistrusts all the clients of the class.

1. He might not trust the callers of the class, so the preconditions of this class need to be checked.
2. Or he might not trust the class to hold the preconditions required by features it calls, so all the preconditions of the features called by this class need to be checked.

The current version of EiffelStudio uses the first approach. When the user indeed mistrusts that the class holds the preconditions of the feature it calls, he needs to enable precondition checking for all the called classes. This will result in a big slow down of the system.

Default settings

When a user creates a new project from scratch, precondition checking is enabled for all the classes in the system. All the other assertion kinds are disabled. First users of EiffelStudio might be very surprised that they never run into any invariant or postcondition violations.

A common pattern for assertion

One would typically completely trust a class from a library provided by a third party and dissable all kinds of assertion checks on the whole library. On the other side