- About This Chapter
- The Customer Manager Example
- Some Questions
- A Contract for CUSTOMER_MANAGER
- The Story So Far
- Runtime Checking
- Trustworthy Documentation
- Summary
- An Aide Memoire
- Things to Do
This chapter is from the book
This chapter is from the book
This chapter is from the book
1.4 A Contract for CUSTOMER_MANAGER
The contract for the customer manager component contains smaller contracts, one for each of the features of the component. (Reminder: For now, a feature is a method or a public, read-only attribute. Sometimes we'll be lazy and talk of "calling a feature," even when we're actually inspecting an attribute.)
We'll explore these smaller contracts one by one. We hope you will concentrate on understanding each contract—don't worry yet about how to write a contract. And keep in mind that we are working on just a fragment of a component (so, for example, we will not discuss how the component is initialized).
By the end of this section, you'll know roughly what a contract is because you'll have seen an example: a contract is a collection of assertions (things that ought to be true) that describe precisely what each feature of the component does and doesn't do.
Adding a New Customer
Here is the contract for the feature you use to add a customer to a customer manager component. It's followed by an explanation.
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 )
The first line is a signature, which names the feature and lists its arguments (here we have just one argument, a_customer). The second line is a comment, which informally describes the feature.
The third line contains the keyword require, which introduces a precondition. A precondition is a condition that a client must be sure is true; otherwise, it is not legal for the client to call the feature (we'll explore later what happens if a client makes an illegal call). On the next line, the identifier id_not_already_active is a tag, or label, chosen by the programmer to improve readability (and to help with debugging—as we will see later). The precondition's assertion is in the next line, and says:
not id_active( a_customer.id )
This asserts that, for it to be legal to call the add feature to add a_customer, it must not be true that the id of a_customer is an active id (we will soon know what makes an id active). The assertion is in Eiffel code so that it can be evaluated at runtime to check whether the client is keeping to its side of the contract.
The keyword ensure introduces a postcondition. A postcondition is a condition that should become true when the feature is executed (otherwise there is a bug in the code that implements the add feature).
In this example, the postcondition contains two assertions, each with its own tag. The first asserts that adding a customer increases the count by one. The expression old count is the value of the count before the feature was called. The = operator is the equality test, not the assignment operator. Asserting that the count now is what it was before, plus one, asserts that it has been increased by one.
The second assertion of the postcondition asserts that the id of the customer passed as argument is now active. This assertion, taken together with the precondition, says that you cannot add a customer if that customer's id is already active, and adding a customer makes that customer's id active.
Now we know the answers to the first two questions we asked earlier.
How do I make an id active? By adding a customer with that id?
Yes.
If I add a customer whose details match an existing customer's details, what happens?
You are not allowed to add a customer whose id equals the id of a customer already owned by the manager. If you keep to this rule, there are no further constraints on whether the name, address, and date of birth can be the same as those of an existing customer.
Setting the Name of a Customer
Here is the contract for the feature you use to set the name of a customer.
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 )
The signature tells us that the feature takes a CUSTOMER_ID and a STRING as arguments.
The precondition (introduced by require) makes it illegal to try to set the name of a customer with an_id that is not active. In other words, it is illegal to try to change the name of a customer that has not been added to the customer manager.
The postcondition (introduced by ensure) asserts that if you now look up the name for the customer with an_id, you'll get back a name that is equal to a_name, the second argument to the set_name feature. In other words, if you set the name of a customer, that's the name the customer now has.
A small detail: Because strings are objects, we assert that we get back a string that is_equal to the name we passed in as argument. One string is_equal to another if they both contain the same characters in the same order. If we'd used the = operator, we would be asserting that we actually get back the string object we passed in. That would be overspecification.
Asking for the Name of a Customer
Here is the contract for the query feature name_for.
name_for( an_id : CUSTOMER_ID ) : STRING -- The name of the customer with 'an_id' require id_active: id_active( an_id )
This time, there is only a precondition, which states that you must not ask for the name for a customer whose id is not active. Why is there no postcondition? Because you are told the value of this query feature in the postcondition of the set_name feature, the feature that defines the value that name_for should have.
Now you know the answers to the third and fourth of your questions.
What do I get if I ask for the name of a customer whose id is not active?
It is illegal to ask for the name of a customer whose id is not active.
What happens if I set the name for a customer whose id is not active?
It is illegal to attempt to set the name of a customer whose id is not active.