This chapter is from the book
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).