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