Code template contract predicate to ensure a value is big enough according to a range's lower bound Eiffel Software big_enough Eiffel code contract invariant precondition postcondition