eiffel-org/documentation/17.05/eiffel/Tutorials/invitation-eiffel-i2e/i2e-design-contract-and-assertions.wiki

[[Property:title|I2E: Design by Contract and Assertions]]
[[Property:weight|-9]]
[[Property:uuid|f563aa75-3a5a-5110-b4f1-07da5448f668]]
If classes are to deserve their definition as abstract data type implementations, they must be known not just by the available operations, but also by the formal properties of these operations, which did not yet appear in the preceding example. 

==The role of assertions==

Eiffel encourages software developers to express formal properties of classes by writing '''assertions''', which may in particular appear in the following roles: <br/>
* Routine '''preconditions''' express the requirements that clients must satisfy whenever they call a routine. For example the designer of <code>ACCOUNT</code> may wish to permit a withdrawal operation only if it keeps the account's balance at or above the minimum. Preconditions are introduced by the keyword <code>require</code>. 
* Routine '''postconditions''', introduced by the keyword <code>ensure</code>, express conditions that the routine (the supplier) guarantees on return, if the precondition was satisfied on entry. 
* A class '''invariant''' must be satisfied by every instance of the class whenever the instance is externally accessible: after creation, and after any call to an exported routine of the class. The invariant appears in a clause introduced by the keyword <code>invariant</code>, and represents a general consistency constraint imposed on all routines of the class. 


With appropriate assertions, the class <code>ACCOUNT</code> becomes: 
<code>
class 
    ACCOUNT

create
    make

feature
        ... Attributes as before:
                balance , minimum_balance , owner , open ...

    deposit (sum: INTEGER)
            -- Deposit sum into the account.
        require
            sum >= 0
        do
            add (sum)
        ensure
            balance = old balance + sum
        end

    withdraw (sum: INTEGER)
            -- Withdraw sum from the account.
        require
            sum >= 0
            sum <= balance - minimum_balance
        do
            add (-sum)
        ensure
            balance = old balance - sum
        end

    may_withdraw ... -- As before

feature {NONE}

    add ... 

    make (initial: INTEGER)
            -- Initialize account with balance initial.
        require
            initial >= minimum_balance
        do
            balance := initial
        end

invariant
    balance >= minimum_balance

end -- ACCOUNT
</code>

The notation <code>old</code> <code>expression</code> is only valid in a routine postcondition. It denotes the value the <code>expression</code> had on routine entry. 

==Creation procedures==

In its last version above, the class now includes a creation procedure, <code>make</code>. With the first version, clients used creation instructions such as <code>create </code> <code>acc1</code> to create accounts; but then the default initialization, setting balance to zero, violated the invariant. By having one or more creation procedures, listed in the <code>create</code> clause at the beginning of the class text, a class offers a way to override the default initializations. The effect of 
<code>
            create acc1.make (5_500)</code>

is to allocate the object (as with the default creation) and to call procedure <code>make</code> on this object, with the argument given. This call is correct since it satisfies the precondition; it will ensure the invariant. 

{{info|The underscore <code>_</code> in the integer constant ''5_500'' has no semantic effect. The general rule is that you can group digits by sets of three from the right to improve the readability of integer constants. }}


Note that the same keyword, <code>create</code>, serves both to introduce creation instructions and the creation clause listing creation procedures at the beginning of the class. 

A procedure listed in the creation clause, such as <code>make</code>, otherwise enjoys the same properties as other routines, especially for calls. Here the procedure <code>make</code> is secret since it appears in a clause starting with 
<code>
feature {NONE}</code>

so it would be invalid for a client to include a call such as 
<code>
            acc.make (8_000)</code>

To make such a call valid, it would suffice to move the declaration of <code>make</code> to the first <code>feature</code> clause of class <code>ACCOUNT</code>, which carries no export restriction. Such a call does not create any new object, but simply resets the balance of a previously created account. 

==Design by Contract&#153;==

Syntactically, assertions are boolean expressions, with a few extensions such as the <code>old </code>notation. Also, you may split an assertion into two or more clauses, as here with the precondition of <code>withdraw</code>; this is as if you had separated the clauses with an <code>and</code>, but makes the assertion clearer, especially if it includes many conditions. 

Assertions play a central part in the Eiffel method for building reliable object-oriented software. They serve to make explicit the assumptions on which programmers rely when they write software elements that they believe are correct. Writing assertions amounts to spelling out the terms of the '''contract''' which governs the relationship between a routine and its callers. The precondition binds the callers; the postcondition binds the routine. 

The underlying theory of Design by Contract&#153;, the centerpiece of the Eiffel method, views software construction as based on contracts between clients (callers) and suppliers (routines), relying on mutual obligations and benefits made explicit by the assertions. 

==The Contract Form==

Assertions are also an indispensable tool for the documentation of reusable software components: one cannot expect large-scale reuse without a precise documentation of what every component expects (precondition), what it guarantees in return (postcondition) and what general conditions it maintains (invariant). 

Documentation tools in EiffelStudio use assertions to produce information for client programmers, describing classes in terms of observable behavior, not implementation. In particular the '''Contract Form''' of a class, also called its "short form", which serves as its interface documentation, is obtained from the full text by removing all non-exported features and all implementation information such as <code>do</code> clauses of routines, but keeping interface information and in particular assertions. Here is the Contract Form of the above class: 
<code>
class interface ACCOUNT

create
    make

feature

    balance: INTEGER
        ...

    deposit (sum: INTEGER)
            -- Deposit sum into the account.
        require
            sum >= 0
        ensure
            balance = old balance + sum

    withdraw (sum: INTEGER)
            -- Withdraw sum from the account.
        require
            sum >= 0
            sum <= balance - minimum_balance
        ensure
            balance = old balance - sum

    may_withdraw ...

end -- ACCOUNT
</code>

This is not actual Eiffel, only documentation of Eiffel classes, hence the use of slightly different syntax to avoid any confusion ( <code>interface class</code> rather than <code>class</code>). In accordance with the Uniform Access Principle (in [[I2E: Classes|Classes]]), the output for <code>balance</code> would be the same if this feature were a function rather than an attribute. 

You will find in EiffelStudio automatic tools to produce the Contract Form of a class. You can also get the '''Flat Contract''' form, based on the same ideas but including inherited features along with those introduced in the class itself. EiffelStudio can produce these forms, and other documentation views of a class, in a variety of output formats including HTML, so that collaborative projects can automatically post the latest versions of their class interfaces on the Internet or an Intranet. 

==Contracts for testing and debugging==

Under EiffelStudio you may also set up compilation options, for the whole system or specific classes only, to evaluate assertions at run time, to uncover potential errors ("bugs"). EiffelStudio provides several levels of assertion monitoring: preconditions only, postconditions etc. When monitoring is on, an assertion which evaluates to true has no further effect on the execution. An assertion that evaluates to false will trigger an exception, as described next; unless you have written an appropriate exception handler, the exception will cause an error message and termination with a precise message and a call trace. 

This ability to check assertions provides a powerful testing and debugging mechanism, in particular because the classes of the EiffelBase Libraries, widely used in Eiffel software development, are protected by carefully written assertions. 

Run-time monitoring, however, is only one application of assertions, whose role as design and documentation aids, as part of the theory of Design by Contract&#153;, exerts a pervasive influence on the Eiffel style of software development.