340 DESIGN BY CONTRACT:BUILDING RELIABLE SOFTWARE $11.5 Both the require and the ensure clauses are optional;when present,they appear at the places shown.The require appears before the local clause,if present.The next sections explain in more detail the meaning of preconditions and postconditions. Note the division into several feature clauses,useful to group the features into categories More on feature cat- indicated by the clauses'header comments.Access,Status report and Element change are egories in“"A stack some of a dozen or so standard categories used throughout the libraries and,whenever class",page 348. applicable,subsequent examples in this book. Preconditions A precondition expresses the constraints under which a routine will function properly. Here: put may not be called if the stack representation is full. remove and item may not be applied to an empty stack. A precondition applies to all calls of the routine,both from within the class and from clients.A correct system will never execute a call in a state that does not satisfy the precondition of the called routine. Postconditions A postcondition expresses properties ofthe state resulting from a routine's execution.Here: After a put,the stack may not be empty,its top is the element just pushed,and its number ofelements has been increased by one. After a remove,the stack may not be full,and its number of elements has been decreased by one. The presence of a postcondition clause in a routine expresses a guarantee on the part of the routine's implementor that the routine will yield a state satisfying certain properties, assuming it has been called with the precondition satisfied. A special notation,old,is available in postconditions;pur and remove use it to express the changes to count.The notation old e,where e is an expression (in most practical cases an attribute),denotes the value that e had on routine entry.Any occurrence of e not preceded by old in the postcondition denotes the value of the expression on exit. The postcondition of put includes the clause count old count +I to state that put,when applied to any object,must increase by one the value of the counr field of that object. A pedagogical note If you are like most software professionals who get exposed to these ideas for the first time,you may be itching to know what effect,if any,the assertions have on the execution of the software,and in particular what happens if one of them gets violated at run time- if full is true when someone calls put,or empry is true when put terminates one of its executions.It is too early to give the full answer but as a preview we can use the lawyer's favorite:it depends.340 DESIGN BY CONTRACT: BUILDING RELIABLE SOFTWARE §11.5 Both the require and the ensure clauses are optional; when present, they appear at the places shown. The require appears before the local clause, if present. The next sections explain in more detail the meaning of preconditions and postconditions. Note the division into several feature clauses, useful to group the features into categories indicated by the clauses’ header comments. Access, Status report and Element change are some of a dozen or so standard categories used throughout the libraries and, whenever applicable, subsequent examples in this book. Preconditions A precondition expresses the constraints under which a routine will function properly. Here: • put may not be called if the stack representation is full. • remove and item may not be applied to an empty stack. A precondition applies to all calls of the routine, both from within the class and from clients. A correct system will never execute a call in a state that does not satisfy the precondition of the called routine. Postconditions A postcondition expresses properties of the state resulting from a routine’s execution. Here: • After a put, the stack may not be empty, its top is the element just pushed, and its number of elements has been increased by one. • After a remove, the stack may not be full, and its number of elements has been decreased by one. The presence of a postcondition clause in a routine expresses a guarantee on the part of the routine’s implementor that the routine will yield a state satisfying certain properties, assuming it has been called with the precondition satisfied. A special notation, old, is available in postconditions; put and remove use it to express the changes to count. The notation old e, where e is an expression (in most practical cases an attribute), denotes the value that e had on routine entry. Any occurrence of e not preceded by old in the postcondition denotes the value of the expression on exit. The postcondition of put includes the clause count = old count + 1 to state that put, when applied to any object, must increase by one the value of the count field of that object. A pedagogical note If you are like most software professionals who get exposed to these ideas for the first time, you may be itching to know what effect, if any, the assertions have on the execution of the software, and in particular what happens if one of them gets violated at run time — if full is true when someone calls put, or empty is true when put terminates one of its executions. It is too early to give the full answer but as a preview we can use the lawyer’s favorite: it depends. More on feature cat￾egories in “A stack class”, page 348