Editing Eiffel (programming language) (section)

===Design by contract===
{{Further|Design by contract}}
The concept of Design by Contract is central to Eiffel. The contracts assert what must be true before a routine is executed (precondition) and what must hold to be true after the routine finishes (post-condition). Class Invariant contracts define what assertions must hold true both before and after any feature of a class is accessed (both routines and attributes). Moreover, contracts codify into executable code developer and designers assumptions about the operating environment of the features of a class or the class as a whole by means of the invariant.

The Eiffel compiler is designed to include the feature and class contracts in various levels. EiffelStudio, for example, executes all feature and class contracts during execution in the "Workbench mode." When an executable is created, the compiler is instructed by way of the project settings file (e.g. ECF file) to either include or exclude any set of contracts. Thus, an executable file can be compiled to either include or exclude any level of contract, thereby bringing along continuous levels of unit and integration testing. Moreover, contracts can be continually and methodically exercised by way of the Auto-Test feature found in EiffelStudio.

The Design by Contract mechanisms are tightly integrated with the language and guide redefinition of features in inheritance:

* Routine precondition: The precondition may only be weakened by inheritance; any call that meets the requirements of the ancestor meets those of the descendant.
* Routine postcondition: The postcondition can only be strengthened by inheritance; any result guaranteed by the ancestor is still provided by the descendant.
* Class invariant: Conditions that must hold true after the object's creation and after any call to an exported class routine. Because the invariant is checked so often, it makes it simultaneously the most expensive and most powerful form of condition or contract.

In addition, the language supports a "check instruction" (a kind of "assert"), loop invariants, and loop variants (which guarantee loop termination).