Editing Precondition (section)

===Eiffel example===
The routine in the following example written in [[Eiffel (programming language)|Eiffel]] takes as an argument an integer which must be a valid value for an hour of the day, i. e., 0 through 23, inclusively. The precondition follows the keyword <code>require</code>. It specifies that the argument must be greater than or equal to zero and less than or equal to 23. The tag "<code>valid_argument:</code>" describes this precondition clause and serves to identify it in case of a runtime precondition violation.

<syntaxhighlight lang="eiffel">
    set_hour (a_hour: INTEGER)
            -- Set `hour' to `a_hour'
        require
            valid_argument: 0 <= a_hour and a_hour <= 23
        do
            hour := a_hour
        ensure
            hour_set: hour = a_hour
        end
</syntaxhighlight>