Home > Articles > Programming

  • Print
  • + Share This
This chapter is from the book

This chapter is from the book

1.5 The Story So Far

Here, in one place, is the contract on the CUSTOMER_MANAGER component, followed by some discussion. There is a new part to the contract, an invariant.

The invariant asserts that count is always zero or greater. An invariant property of a component is always true (more precisely, it is true whenever you can call a feature on the component).

component CUSTOMER_MANAGER

	count : INTEGER
			-- The number of customers

	id_active( an_id : CUSTOMER_ID ) : BOOLEAN
			-- Is there a customer with 'an_id'?

	add( a_customer : BASIC_CUSTOMER_DETAILS )
			-- Add 'a_customer' to the set of customers
		require
			id_not_already_active:
				 not id_active( a_customer.id )
		ensure
			count_increased: 
				count = old count + 1
			customer_id_now_active:
				 id_active( a_customer.id )
		
	name_for( an_id : CUSTOMER_ID ) : STRING
			-- The name of the customer with 'an_id'
		require
			id_active: 
				id_active( an_id )

	set_name( an_id : CUSTOMER_ID; a_name : STRING )
			-- Set the name of the customer with 'an_id' to 'a_name'
		require
			id_active: 
				id_active( an_id ) 
		ensure
			name_set:
				 name_for( an_id ).is_equal( a_name )									
	...
 invariant
	count_never_negative:
		count >= 0
end

The contract is definitely unfinished. It still leaves many questions unanswered, but we hope you can see that a contract can answer many of the questions that a client programmer might ask.

The syntax of the component contract is that of the programming language Eiffel (except for the first line—Eiffel doesn't have special syntax to distinguish a component from a class).

The features count and id_active have neither preconditions nor postconditions. They don't have preconditions because it is always legal to call them. They don't have postconditions because their values are defined elsewhere. Specifically, the postcondition on the add_customer feature defines that add_customer both increments the count and makes id_active for the id of the added customer.

Notice how different parts of the component and its contract cannot be discussed in isolation. For example, the name returned by the name_for query feature is defined in the postcondition of the set_name feature. We cannot define the name_for some id without discussing the feature that sets it. Conversely, we cannot define what name is set for a customer by set_name without discussing the name_for query that tells us the name for the particular customer.

That's why we say that the component has a single contract (which, in turn, is made up of the individual contracts on the individual features).

  • + Share This
  • 🔖 Save To Your Account