[Eiffel] design by contract

This is a very simple example. There are two levels of contract.

• The contract for set_val routine: require states the precondition of this routine that the argument v shall not be negative; ensure enforces the postcondition of this routine that the val shall be equal to v. 
• Class invariant enforces that for all objects/instances of this class their val shall not be negative.

The do  clause actually is an implementation of the specification, expressed by precondition and postcondition, of reset or set_val. If the implementation violates the specification, then bugs are found. This concept is similar to the refinement check in B method. When we regard class in Eiffel as a B machine, member features map to variables in B, create maps to initialisation in B and invariant to invariant. However in B method, a specification and its implementation are in different machine but Eiffel takes them together.

In B method, it can check the correctness between the implementation and the specification by a theorem prover or a model checker. In Eiffel, it might use the hybrid method (static analysis plus test run) to check it.

If we can write the specification in B method (or similar formal languages such as Z notation, VDM), then refine them to an implementation by the refinement check. Afterwards, we may translate this refinement to Eiffel language and also keep the specification. It might be a good way from a formal specification, formal verification and finally to the code.