Contracts in Eiffel

• "preconditions" and "postconditions"

decrement is
    require
        item > 0
    do
        item := item - 1
    ensure
        item = old item - 1
    end