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