Reading Design by Contract tutorial I stumbled upon the following line:
Contracts in Eiffel are not just wishful thinking. They can be monitored at run time under the control of compilation options.
followed by explanations that they will throw exceptions when fail. It makes me think that all the require ensure invariant all checks can be either performed at runtime or turned off. Is this correct? Or they can be enforced at compile time as well using appropriate compiler options?
There is a tool AutoProof for verifying contracts at compile time. It performs some transformations ending up with an SMT instance that is checked by the Z3 SMT solver that tells whether all assertions hold. From the brief introduction, it follows that quite a bit of annotations is required to use it. Nevertheless, the tool was used to verify Base2, a set of container classes, similar to the standard classes of the Base library. The contracts rely on a so called Semantic Collaboration technique described in the corresponding papers (look for Publications at the AutoProof page).
There is some ongoing research work to simplify techniques employed by AutoProof, fix existing issues, adapt it for use with void-safe systems and SCOOP (Simple Concurrent Object-Oriented Programming). As of time of writing, the technology is still in the research stage and is not ready for prime use in a production environment. The main obstacle is complexity and special training required to use the technology. However, the basic ideas are pretty general that allows for using the tool in teaching process.
