Contract checking for Vaucanson
[Miscellaneous constructs used by Vaucanson]
|
Assertions
Assertions are a weak kind of contract that states that a specified property must hold.
A failed assertion should always mean that an internal inconsistency has been detected, caused by a software (or hardware) bug.
Preconditions
Preconditions ensure that the prerequisites for using a function or instanciating a template are fulfilled.
Breach of a precondition should prevent the library user from using a feature, either generating a type error for forbidden template instanciations or run-type exception at function entry.
Postconditions
Postconditions ensure that the result of a computation exhibits the specified properties.
Breach of a postcondition should show that an algorithm is bogus.
Call to pure abstract services
Some services are purely abstract and should not be called directly. In most cases this kind of information is expressed through C++ typing.
Warnings
In addition to contracts, the library is equiped with mechanisms intended to inform the user of misbehaviors, undocumented properties, deprecated features and so on.
Recommendations
Recommendations are a kind of assertions that do not cause the program to stop. A failed recommendation will only output a warning onto the error stream. It means that not respecting the condition might be dangerous under certain circumstances, but may work if you know what you are doing.
Breach of a recommendation means you are doing something potentially dangerous.
Deprecated features
Deprecated features are features that have been superceded by others, and intended to be removed at some point.
Weak implementations
Weak implementations are code pieces written to ensure that a specified feature is provided, but was not tested for full conformance.
Weak implementations should work with most trivial cases but denote a library weakness on which the developers will focus.
Incomplete implementation
Incomplete implementations are code pieces written to ensure that a specified expressivity is provided, but without providing the actual feature.
