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