Difference between revisions of "Assertion Settings"
m (→Proposal for a property: Supplier_invariants) |
m (→Agents) |
||
| (16 intermediate revisions by 2 users not shown) | |||
| Line 1: | Line 1: | ||
Author: Matthias Konrad | Author: Matthias Konrad | ||
| + | |||
| + | [[Category:Assertion checking]] | ||
==Introduction== | ==Introduction== | ||
| Line 7: | Line 9: | ||
* Postconditions | * Postconditions | ||
* Invariants | * Invariants | ||
| − | * Loop variants | + | * Loop variants/invariants |
* Checks | * 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 | + | 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 necessary 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. | 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. | ||
| Line 17: | Line 19: | ||
==Proposal for a property: Supplier_preconditions== | ==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: | + | 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, since he might violate preconditions of the called features. 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.) | * 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. | * 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 | + | It would thus be nice if one could specify for a class, that all the preconditions of its called features are checked. Not always, 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. Such a property could be called '''Supplier_preconditions'''. |
| − | + | The following picture shows one class with this property enabled and one that has it disabled: | |
| − | + | ||
| − | + | ||
| − | + | [[Image:SupplierPrecond.jpg]] | |
| + | The arrows show whether the preconditions need to be checked for a given caller (tail of the arrow) and a callee (peak of the arrow). | ||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
====Default settings==== | ====Default settings==== | ||
| − | When a user creates a new project from scratch | + | When a user creates a new project from scratch he uses a template config file. This template should per default disable all assertion kinds for all the library classes and enable all assertion kinds on the root cluster (including the new Supplier_preconditions property). |
| − | + | ||
| − | + | ||
| − | + | ||
| − | + | ||
| − | + | ||
| − | + | ||
| − | + | ||
Latest revision as of 07:42, 1 November 2006
Author: Matthias Konrad
Introduction
The Eiffel Language specifies several assertion types:
- Preconditions
- Postconditions
- Invariants
- Loop variants/invariants
- 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 necessary 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, since he might violate preconditions of the called features. 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 always, 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. Such a property could be called Supplier_preconditions.
The following picture shows one class with this property enabled and one that has it disabled:
The arrows show whether the preconditions need to be checked for a given caller (tail of the arrow) and a callee (peak of the arrow).
Default settings
When a user creates a new project from scratch he uses a template config file. This template should per default disable all assertion kinds for all the library classes and enable all assertion kinds on the root cluster (including the new Supplier_preconditions property).
