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