Code template contract predicate to ensure a value is small enough according to a range's upper bound Eiffel Software small_enough Eiffel code contract invariant precondition postcondition