Code template contract predicate for ensuring an entity is a negative numerical Eiffel Software is_neg Eiffel code contract invariant precondition postcondition