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