342 DESIGN BY CONTRACT:BUILDING RELIABLE SOFTWARE $11.6 In relations between people or companies,a contract is a written document that serves to clarify the terms of a relationship.It is really surprising that in software,where precision is so important and ambiguity so risky,this idea has taken so long to impose itself.A precondition-postcondition pair for a routine will describe the contract that the routine(the supplier of a certain service)defines for its callers (the clients of that service). Perhaps the most distinctive feature ofcontracts as they occur in human affairs is that any good contract entails obligations as well as benefits for both parties-with an obligation for one usually turning into a benefit for the other.This is true of contracts between classes,too: The precondition binds the client:it defines the conditions under which a call to the routine is legitimate.It is an obligation for the client and a benefit for the supplier. The postcondition binds the class:it defines the conditions that must be ensured by the routine on return.It is a benefit for the client and an obligation for the supplier. The benefits are,for the client,the guarantee that certain properties will hold after the call;for the supplier,the guarantee that certain assumptions will be satisfied whenever the routine is called.The obligations are,for the client,to satisfy the requirements as stated by the precondition;for the supplier,to do the job as stated by the postcondition. Here is the contract for one of the routines in our example: put OBLIGATIONS BENEFITS A routine contract: (Satisfy precondition:) (From postcondition:) routine put for Client Only call put (x)on a non- Get stack updated:not a stack class full stack. empty,x on top(item yields x,count increased by 1). Supplier (Satisfy postcondition:) (From precondition:) Update stack representation Simpler processing thanks to have x on top(item yields to the assumption that stack x),count increased by 1, is not full. not empty. Zen and the art of software reliability:guaranteeing more by checking less Although you may not have noticed it yet,one of the contract rules given goes against the generally accepted wisdom in software engineering;shocking at first to many,it is among the method's main contributions to software reliability and deserves emphasis. The rule reflects the above observation that the precondition is a benefit for the supplier and is expressed in the bottom-right box of the table:if the client's part of the342 DESIGN BY CONTRACT: BUILDING RELIABLE SOFTWARE §11.6 In relations between people or companies, a contract is a written document that serves to clarify the terms of a relationship. It is really surprising that in software, where precision is so important and ambiguity so risky, this idea has taken so long to impose itself. A precondition-postcondition pair for a routine will describe the contract that the routine (the supplier of a certain service) defines for its callers (the clients of that service). Perhaps the most distinctive feature of contracts as they occur in human affairs is that any good contract entails obligations as well as benefits for both parties — with an obligation for one usually turning into a benefit for the other. This is true of contracts between classes, too: • The precondition binds the client: it defines the conditions under which a call to the routine is legitimate. It is an obligation for the client and a benefit for the supplier. • The postcondition binds the class: it defines the conditions that must be ensured by the routine on return. It is a benefit for the client and an obligation for the supplier. The benefits are, for the client, the guarantee that certain properties will hold after the call; for the supplier, the guarantee that certain assumptions will be satisfied whenever the routine is called. The obligations are, for the client, to satisfy the requirements as stated by the precondition; for the supplier, to do the job as stated by the postcondition. Here is the contract for one of the routines in our example: Zen and the art of software reliability: guaranteeing more by checking less Although you may not have noticed it yet, one of the contract rules given goes against the generally accepted wisdom in software engineering; shocking at first to many, it is among the method’s main contributions to software reliability and deserves emphasis. The rule reflects the above observation that the precondition is a benefit for the supplier and is expressed in the bottom-right box of the table: if the client’s part of the put OBLIGATIONS BENEFITS Client (Satisfy precondition:) Only call put (x) on a non￾full stack. (From postcondition:) Get stack updated: not empty, x on top (item yields x, count increased by 1). Supplier (Satisfy postcondition:) Update stack representation to have x on top (item yields x), count increased by 1, not empty. (From precondition:) Simpler processing thanks to the assumption that stack is not full. A routine contract: routine put for a stack class