Code template contract predicate ensuring if an entity is a non-positive (zero or negative) numeric Eiffel Software not_is_neg Eiffel code contract invariant precondition postcondition