336 DESIGN BY CONTRACT:BUILDING RELIABLE SOFTWARE $11.3 The precondition first.From the viewpoint of the prospective employee-the person who has to perform what has been called 4-the precondition P defines the conditions under which the required job will start or,to put it differently,the set of cases that have to be handled.So a strong P is good news:it means that you only have to deal with a limited set of situations.The stronger the P,the easier for the employee.In fact,the perfect sinecure is the job defined by Sinecure 1 False A... The postcondition has been left unspecified because it does not matter what it is. Indeed if you ever see such an ad,do not even bother reading the postcondition;take the job right away.The precondition False is the strongest possible assertion,since it is never satisfied in any state.Any request to execute 4 will be incorrect,and the fault lies not with the agent responsible for 4 but with the requester-the client-since it did not observe the required precondition,for the good reason that it is impossible to observe it.Whatever A does or does not do may be useless,but is always correct-in the sense,defined earlier, of being consistent with the specification. The above job specification is probably what a famous police chief of a Southern US city had in mind,a long time ago,when,asked by an interviewer why he had chosen his career,he replied:"Obvious-it is the only job where the customer is always wrong". For the postcondition O,the situation is reversed.A strong postcondition is bad news:it indicates that you have to deliver more results.The weaker the O,the better for the employee.In fact,the second best sinecure in the world is the job defined,regardless of the precondition,by Sinecure 2 (..A (True) The postcondition True is the weakest possible assertion,satisfied by all states. The notions of "stronger"and "weaker"are formally defined from logic:P/is said to be stronger than P2,and P2 weaker than P/,if P/implies P2 and they are notequal.As every proposition implies True,and False implies every proposition,it is indeed legitimate to speak of True as the weakest and False as the strongest of all possible assertions. Why,by the way,is Sinecure 2 only the"second best"job in the world?The reason has to do with a fine point that you may have noticed in the definition of the meaning of (P)4O)on the preceding page:termination.The definition stated that the execution must terminate in a state satisfying O whenever it is started in a state satisfying P.With Sinecure 1 there are no states satisfying P,so it does not matter what 4 does,even if it is a program text whose execution would go into an infinite loop or crash the computer.Any A will be "correct"with respect to the given specification.With Sinecure 2,however,there
336 DESIGN BY CONTRACT: BUILDING RELIABLE SOFTWARE §11.3 The precondition first. From the viewpoint of the prospective employee — the person who has to perform what has been called A — the precondition P defines the conditions under which the required job will start or, to put it differently, the set of cases that have to be handled. So a strong P is good news: it means that you only have to deal with a limited set of situations. The stronger the P, the easier for the employee. In fact, the perfect sinecure is the job defined by The postcondition has been left unspecified because it does not matter what it is. Indeed if you ever see such an ad, do not even bother reading the postcondition; take the job right away. The precondition False is the strongest possible assertion, since it is never satisfied in any state. Any request to execute A will be incorrect, and the fault lies not with the agent responsible for A but with the requester — the client — since it did not observe the required precondition, for the good reason that it is impossible to observe it. Whatever A does or does not do may be useless, but is always correct — in the sense, defined earlier, of being consistent with the specification. The above job specification is probably what a famous police chief of a Southern US city had in mind, a long time ago, when, asked by an interviewer why he had chosen his career, he replied: “Obvious — it is the only job where the customer is always wrong”. For the postcondition Q, the situation is reversed. A strong postcondition is bad news: it indicates that you have to deliver more results. The weaker the Q, the better for the employee. In fact, the second best sinecure in the world is the job defined, regardless of the precondition, by The postcondition True is the weakest possible assertion, satisfied by all states. The notions of “stronger” and “weaker” are formally defined from logic: P1 is said to be stronger than P2, and P2 weaker than P1, if P1 implies P2 and they are not equal. As every proposition implies True, and False implies every proposition, it is indeed legitimate to speak of True as the weakest and False as the strongest of all possible assertions. Why, by the way, is Sinecure 2 only the “second best” job in the world? The reason has to do with a fine point that you may have noticed in the definition of the meaning of {P} A {Q} on the preceding page: termination. The definition stated that the execution must terminate in a state satisfying Q whenever it is started in a state satisfying P. With Sinecure 1 there are no states satisfying P, so it does not matter what A does, even if it is a program text whose execution would go into an infinite loop or crash the computer. Any A will be “correct” with respect to the given specification. With Sinecure 2, however, there Sinecure 1 {False} A {…} Sinecure 2 {…} A {True}
$11.4 INTRODUCING ASSERTIONS INTO SOFTWARE TEXTS 337 must be a final state;that state does not need to satisfy any specific properties,but it must exist.From the viewpoint of whoever has to perform 4:you need to do nothing,but you must do it in finite time. Readers familiar with theoretical computing science or program proving techniques will have noted that the P)4O)notation as used here denotes total correctness,which includes termination as well as conformance to specification.(The property that a program will satisfy its specification if it terminates is known as partial correctness.)See [M 1990]for a detailed presentation of these concepts. The discussion of whether a stronger or weaker assertion is"bad news"or"good news" has taken the viewpoint of the prospective employee.If,changing sides,we start looking at the situation as if we were the employer,everything is reversed:a weaker precondition will be good news,as it means ajob that handles a broader set of input cases;so will be a stronger postcondition,as it means more significant results.This reversal of criteria is typical of discussions of software correctness,and will reappear as the central notion of this chapter: contracts between client and supplier modules,in which a benefit for one is an obligation for the other.To produce effective and reliable software is to draw up the contract representing the best possible compromise in all applicable client-supplier communications. 11.4 INTRODUCING ASSERTIONS INTOSOFTWARE TEXTS Once we have defined the correctness of a software element as the consistency of its implementation with its specification,we should take steps to include the specification, together with the implementation,in the software itself.For most of the software community this is still a novel idea:we are accustomed to programs as defining the operations that we command our hardware-software machines to execute for us(the how); it is less common to treat the description of the software's purposes (the what)as being part of the software itself. To express the specification,we will rely on assertions.An assertion is an expression involving some entities of the software,and stating a property that these entities may satisfy at certain stages of software execution.A typical assertion might express that a certain integer has a positive value or that a certain reference is not void. Mathematically,the closest notion is that of predicate,although the assertion language that we shall use has only part of the power of full predicate calculus. Syntactically,the assertions of our notation will simply be boolean expressions,with a few extensions.One of these extensions,the old notation,is introduced later in this chapter.Another is the use of the semicolon,as in n>0;x=Void The meaning of the semicolon is equivalent to that of an and.As between declarations and instructions,the semicolon is actually optional,and we will om it it when assertion clauses appear on separate lines;just consider that there is an implicit and between successive assertion lines.These conventions facilitate identification of the individual components ofan assertion.It is indeed possible,and usually desirable,to label these components individually,as in
§11.4 INTRODUCING ASSERTIONS INTO SOFTWARE TEXTS 337 must be a final state; that state does not need to satisfy any specific properties, but it must exist. From the viewpoint of whoever has to perform A: you need to do nothing, but you must do it in finite time. Readers familiar with theoretical computing science or program proving techniques will have noted that the {P} A {Q} notation as used here denotes total correctness, which includes termination as well as conformance to specification. (The property that a program will satisfy its specification if it terminates is known as partial correctness.) See [M 1990] for a detailed presentation of these concepts. The discussion of whether a stronger or weaker assertion is “bad news” or “good news” has taken the viewpoint of the prospective employee. If, changing sides, we start looking at the situation as if we were the employer, everything is reversed: a weaker precondition will be good news, as it means a job that handles a broader set of input cases; so will be a stronger postcondition, as it means more significant results. This reversal of criteria is typical of discussions of software correctness, and will reappear as the central notion of this chapter: contracts between client and supplier modules, in which a benefit for one is an obligation for the other. To produce effective and reliable software is to draw up the contract representing the best possible compromise in all applicable client-supplier communications. 11.4 INTRODUCING ASSERTIONS INTO SOFTWARE TEXTS Once we have defined the correctness of a software element as the consistency of its implementation with its specification, we should take steps to include the specification, together with the implementation, in the software itself. For most of the software community this is still a novel idea: we are accustomed to programs as defining the operations that we command our hardware-software machines to execute for us (the how); it is less common to treat the description of the software’s purposes (the what) as being part of the software itself. To express the specification, we will rely on assertions. An assertion is an expression involving some entities of the software, and stating a property that these entities may satisfy at certain stages of software execution. A typical assertion might express that a certain integer has a positive value or that a certain reference is not void. Mathematically, the closest notion is that of predicate, although the assertion language that we shall use has only part of the power of full predicate calculus. Syntactically, the assertions of our notation will simply be boolean expressions, with a few extensions. One of these extensions, the old notation, is introduced later in this chapter. Another is the use of the semicolon, as in n > 0 ; x /= Void The meaning of the semicolon is equivalent to that of an and. As between declarations and instructions, the semicolon is actually optional, and we will omit it when assertion clauses appear on separate lines; just consider that there is an implicit and between successive assertion lines. These conventions facilitate identification of the individual components of an assertion. It is indeed possible, and usually desirable, to label these components individually, as in
338 DESIGN BY CONTRACT:BUILDING RELIABLE SOFTWARE $11.5 Positive:n>0 Not void:x /Void If present,the labels(such as Positive and Not void in this example)will play a role in the run-time effect of assertions-to be discussed later in this chapter-but for the moment they are mainly there for clarity and documentation. The next few sections will review this principal application of assertions:as a conceptual tool enabling software developers to construct correct systems and to document why they are correct. 11.5 PRECONDITIONS AND POSTCONDITIONS The first use of assertions is the semantic specification of routines.A routine is not just a piece of code;as the implementation of some function from an abstract data type specification,it should perform a useful task.It is necessary to express this task precisely, both as an aid in designing it (you cannot hope to ensure that a routine is correct unless you have specified what it is supposed to do)and,later,as an aid to understanding its text. You may specify the task performed by a routine by two assertions associated with the routine:a precondition and a postcondition.The precondition states the properties that must hold whenever the routine is called;the postcondition states the properties that the routine guarantees when it returns. A stack class An example will enable us to become familiar with the practical use of assertions.In the previous chapter,we saw the outline of a generic stack class,under the form class STACK [G]feature ..Declaration of the features: count,empty,full,put,remove,item end An implementation will appear below.Before considering implementation issues, however,it is important to note that the routines are characterized by strong semantic properties,independent of any specific representation.For example: Routines remove and item are only applicable if the number ofelements is not zero. put increases the number ofelements by one;remove decreases it by one. Such properties are part of the abstract data type specification,and even people who do not use any approach remotely as formal as ADTs understand them implicitly.But in common approaches to software construction software texts reveal no trace of them. Through routine preconditions and postconditions you can turn them into explicit elements of the software. We will express preconditions and postconditions as clauses of routine declarations introduced by the keywords require and ensure respectively.For the stack class,leaving the routine implementations blank for the time being,this gives:
338 DESIGN BY CONTRACT: BUILDING RELIABLE SOFTWARE §11.5 Positive: n > 0 Not_void: x /= Void If present, the labels (such as Positive and Not_void in this example) will play a role in the run-time effect of assertions — to be discussed later in this chapter — but for the moment they are mainly there for clarity and documentation. The next few sections will review this principal application of assertions: as a conceptual tool enabling software developers to construct correct systems and to document why they are correct. 11.5 PRECONDITIONS AND POSTCONDITIONS The first use of assertions is the semantic specification of routines. A routine is not just a piece of code; as the implementation of some function from an abstract data type specification, it should perform a useful task. It is necessary to express this task precisely, both as an aid in designing it (you cannot hope to ensure that a routine is correct unless you have specified what it is supposed to do) and, later, as an aid to understanding its text. You may specify the task performed by a routine by two assertions associated with the routine: a precondition and a postcondition. The precondition states the properties that must hold whenever the routine is called; the postcondition states the properties that the routine guarantees when it returns. A stack class An example will enable us to become familiar with the practical use of assertions. In the previous chapter, we saw the outline of a generic stack class, under the form class STACK [G] feature … Declaration of the features: count, empty, full, put, remove, item end An implementation will appear below. Before considering implementation issues, however, it is important to note that the routines are characterized by strong semantic properties, independent of any specific representation. For example: • Routines remove and item are only applicable if the number of elements is not zero. • put increases the number of elements by one; remove decreases it by one. Such properties are part of the abstract data type specification, and even people who do not use any approach remotely as formal as ADTs understand them implicitly. But in common approaches to software construction software texts reveal no trace of them. Through routine preconditions and postconditions you can turn them into explicit elements of the software. We will express preconditions and postconditions as clauses of routine declarations introduced by the keywords require and ensure respectively. For the stack class, leaving the routine implementations blank for the time being, this gives:
$11.5 PRECONDITIONS AND POSTCONDITIONS 339 indexing description:"Stacks:Dispenser structures with a Last-In,First-Out %access policy" class STACKI [G]feature Access count:INTEGER --Number of stack elements item:G is --Top element require not empty do end feature --Status report empty:BOOLEAN is -Is stack empty? do...end full:BOOLEAN is --Is stack representation full? do end feature--Element change put (x:G)is --Add x on top. require not full do ensure not empty item=x count old count +I end remove is --Remove top element. require not empry do ensure not full cout old count-I end end
§11.5 PRECONDITIONS AND POSTCONDITIONS 339 indexing description: "Stacks: Dispenser structures with a Last-In, First-Out % %access policy" class STACK1 [G] feature -- Access count: INTEGER -- Number of stack elements item: G is -- Top element require not empty do … end feature -- Status report empty: BOOLEAN is -- Is stack empty? do … end full: BOOLEAN is -- Is stack representation full? do … end feature -- Element change put (x: G) is -- Add x on top. require not full do … ensure not empty item = x count = old count + 1 end remove is -- Remove top element. require not empty do … ensure not full count = old count – 1 end end
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 categories in “A stack class”, page 348