Invariants

• Back to Eiffel for a second:

class MUTABLE_NUMBER feature
    decrement is
        ...

    invariant
        item > 0
end