Count Is Positive Code template contract predicate to ensure an entity's count is greater than zero Eiffel Software pos_count Eiffel code contract invariant precondition postcondition A variable to test for a positive count on