Design by Contract: building reliable software quippeth th basieoneptsof cassobectd you cn byo software modules that implement possibly parameterized types of data structures. Congratulations.This is a significant step in the quest for better software architectures. But the techniques seen so far are not sufficient to implement the comprehensive view of quality introduced at the beginning of this book.The quality factors on which we have concentrated-reusability,extendibility,compatibility-must not be attained at the expense of reliability (correctness and robustness).Although,as recalled next,the reliability concern was visible in many aspects of the discussion,we need more The need to pay more attention to the semantic properties of our classes will be particularly clear if you remember how classes were defined:as implementations of abstract data types.The classes seen so far consist of attributes and routines,which indeed represent the functions of an ADT specification.But an ADT is more than just a list of available operations:remember the role played by the semantic properties,as expressed by the axioms and preconditions.They are essential to capture the true nature of the type's instances.In studying classes,we have-temporarily-lost sight of this semantic aspect of the ADT concept.We will need to bring it back into the method if we want our software to be not just flexible and reusable,but also correct and robust. Assertions and the associated concepts,explained in this chapter,provide some of the answer.Although not foolproof,the mechanisms presented below provide the programmer with essential tools for expressing and validating correctness arguments.The key concept will be Design by Contract:viewing the relationship between a class and its clients as a formal agreement,expressing each party's rights and obligations.Only through such a precise definition of every module's claims and responsibilities can we hope to attain a significant degree of trust in large software systems. In reviewing these concepts,we shall also encounter a key problem of software engineering:how to deal with run-time errors-with contract violations.This leads to the subject of exception handling,covered in the next chapter.The distribution of roles between the two chapters roughly reflects the distinction between the two components of reliability;as you will recall,correctness was defined as the software's ability to perform according to its specification,and robustness as its ability to react to cases not included in the specification.Assertions (this chapter)generally cover correctness,and exceptions (next chapter)generally cover robustness
11 Design by Contract: building reliable software Equipped with the basic concepts of class, object and genericity, you can by now write software modules that implement possibly parameterized types of data structures. Congratulations. This is a significant step in the quest for better software architectures. But the techniques seen so far are not sufficient to implement the comprehensive view of quality introduced at the beginning of this book. The quality factors on which we have concentrated — reusability, extendibility, compatibility — must not be attained at the expense of reliability (correctness and robustness). Although, as recalled next, the reliability concern was visible in many aspects of the discussion, we need more. The need to pay more attention to the semantic properties of our classes will be particularly clear if you remember how classes were defined: as implementations of abstract data types. The classes seen so far consist of attributes and routines, which indeed represent the functions of an ADT specification. But an ADT is more than just a list of available operations: remember the role played by the semantic properties, as expressed by the axioms and preconditions. They are essential to capture the true nature of the type’s instances. In studying classes, we have — temporarily — lost sight of this semantic aspect of the ADT concept. We will need to bring it back into the method if we want our software to be not just flexible and reusable, but also correct and robust. Assertions and the associated concepts, explained in this chapter, provide some of the answer. Although not foolproof, the mechanisms presented below provide the programmer with essential tools for expressing and validating correctness arguments. The key concept will be Design by Contract: viewing the relationship between a class and its clients as a formal agreement, expressing each party’s rights and obligations. Only through such a precise definition of every module’s claims and responsibilities can we hope to attain a significant degree of trust in large software systems. In reviewing these concepts, we shall also encounter a key problem of software engineering: how to deal with run-time errors — with contract violations. This leads to the subject of exception handling, covered in the next chapter. The distribution of roles between the two chapters roughly reflects the distinction between the two components of reliability; as you will recall, correctness was defined as the software’s ability to perform according to its specification, and robustness as its ability to react to cases not included in the specification. Assertions (this chapter) generally cover correctness, and exceptions (next chapter) generally cover robustness
332 DESIGN BY CONTRACT:BUILDING RELIABLE SOFTWARE $11.1 Some important extensions to the basic ideas of Design by Contract will have to wait until the presentation of inheritance,polymorphism and dynamic binding,enabling us to go from contracts to subcontracting. 11.1 BASIC RELIABILITY MECHANISMS The preceding chapters already introduced a set of techniques that directly address the goal of producing reliable software.Let us review them briefly;it would be useless to consider more advanced concepts until we have put in place all the basic reliability mechanisms. First,the defining property of object technology is an almost obsessive concern with the structure of software systems.By defining simple,modular,extendible architectures, we make it easier to ensure reliability than with contorted structures as often result from earlier methods.In particular the effort to limit inter-module communication to the strict minimum was central to the discussion of modularity that got us started;it resulted in the prohibition of such common reliability risks as global variables,and in the definition of restricted communication mechanisms,the client and inheritance relations.The general observation is that the single biggest enemy ofreliability(and perhaps of software quality in general)is complexity.Keeping our structures as simple as possible is not enough to ensure reliability,but it is a necessary condition.So the discussion of the previous chapters provides the right starting point for the systematic effort of the present one. Also necessary if not sufficient is the constant emphasis on making our software elegant and readable.Software texts are not just written,they are read and rewritten many times;clarity and simplicity of notation,such as have been attempted in the language constructs introduced so far,are a required basis for any more sophisticated approach to reliability. Another indispensable weapon is automatic memory management,specifically garbage collection.The chapter on memory management explained in detail why,for any system that creates and manipulates dynamic data structures,it would be dangerous to rely on manual reclamation (or no reclamation).Garbage collection is not a luxury;it is a crucial reliability-enhancing component of any O-O environment. The same can be said of another technique presented (in connection with genericity) in the last chapter:static typing.Without statically enforced type rules,we would be at the mercy of run-time typing errors. All these techniques provide the necessary basis,from which we can now take a closer look at what it will take for a software system to be correct and robust
332 DESIGN BY CONTRACT: BUILDING RELIABLE SOFTWARE §11.1 Some important extensions to the basic ideas of Design by Contract will have to wait until the presentation of inheritance, polymorphism and dynamic binding, enabling us to go from contracts to subcontracting. 11.1 BASIC RELIABILITY MECHANISMS The preceding chapters already introduced a set of techniques that directly address the goal of producing reliable software. Let us review them briefly; it would be useless to consider more advanced concepts until we have put in place all the basic reliability mechanisms. First, the defining property of object technology is an almost obsessive concern with the structure of software systems. By defining simple, modular, extendible architectures, we make it easier to ensure reliability than with contorted structures as often result from earlier methods. In particular the effort to limit inter-module communication to the strict minimum was central to the discussion of modularity that got us started; it resulted in the prohibition of such common reliability risks as global variables, and in the definition of restricted communication mechanisms, the client and inheritance relations. The general observation is that the single biggest enemy of reliability (and perhaps of software quality in general) is complexity. Keeping our structures as simple as possible is not enough to ensure reliability, but it is a necessary condition. So the discussion of the previous chapters provides the right starting point for the systematic effort of the present one. Also necessary if not sufficient is the constant emphasis on making our software elegant and readable. Software texts are not just written, they are read and rewritten many times; clarity and simplicity of notation, such as have been attempted in the language constructs introduced so far, are a required basis for any more sophisticated approach to reliability. Another indispensable weapon is automatic memory management, specifically garbage collection. The chapter on memory management explained in detail why, for any system that creates and manipulates dynamic data structures, it would be dangerous to rely on manual reclamation (or no reclamation). Garbage collection is not a luxury; it is a crucial reliability-enhancing component of any O-O environment. The same can be said of another technique presented (in connection with genericity) in the last chapter: static typing. Without statically enforced type rules, we would be at the mercy of run-time typing errors. All these techniques provide the necessary basis, from which we can now take a closer look at what it will take for a software system to be correct and robust
$11.2 ABOUT SOFTWARE CORRECTNESS 333 11.2 ABOUT SOFTWARE CORRECTNESS We should first ask ourselves what it means for a software element to be correct.The observations and deductions that will help answer this question will seem rather trivial at first;but let us not forget the comment (made once by a very famous scientist)that scientific reasoning is nothing but the result of starting from ordinary observations and continuing with simple deductions-only very patiently and stubbornly. Assume someone comes to you with a 300,000-line C program and asks you"Is this program correct?".There is not much you can answer.(Ifyou are a consultant,though,try answering"no"and charging a high fee.You might just be right.) To consider the question meaningful,you would need to get not only the program but also a precise description of what it is supposed to do-a specification. The same comment is applicable,of course,regardless of the size of a program.The instructionx=y+/is neither correct nor incorrect;these notions only make sense with respect to a statement of what one expects from the instruction-what effect it is intended to have on the state of the program variables.The instruction is correct for the specification "Make sure that x and y have different values" but it is incorrect vis-a-vis the specification “Make sure that x has a negative value” (since,assuming that the entities involved are integers,x may end up being non-negative after the assignment,depending on the value of y). These examples illustrate the property that must serve as the starting point of any discussion of correctness: Software Correctness property Correctness is a relative notion. A software system or software element is neither correct nor incorrect per se;it is correct or incorrect with respect to a certain specification.Strictly speaking,we should not discuss whether software elements are correct,but whether they are consistent with their specifications.This discussion will continue to use the well-accepted term "correctness", but we should always remember that the question of correctness does not apply to software elements;it applies to pairs made of a software element and a specification
§11.2 ABOUT SOFTWARE CORRECTNESS 333 11.2 ABOUT SOFTWARE CORRECTNESS We should first ask ourselves what it means for a software element to be correct. The observations and deductions that will help answer this question will seem rather trivial at first; but let us not forget the comment (made once by a very famous scientist) that scientific reasoning is nothing but the result of starting from ordinary observations and continuing with simple deductions — only very patiently and stubbornly. Assume someone comes to you with a 300,000-line C program and asks you “Is this program correct?”. There is not much you can answer. (If you are a consultant, though, try answering “no” and charging a high fee. You might just be right.) To consider the question meaningful, you would need to get not only the program but also a precise description of what it is supposed to do — a specification. The same comment is applicable, of course, regardless of the size of a program. The instruction x := y + 1 is neither correct nor incorrect; these notions only make sense with respect to a statement of what one expects from the instruction — what effect it is intended to have on the state of the program variables. The instruction is correct for the specification “Make sure that x and y have different values” but it is incorrect vis-à-vis the specification “Make sure that x has a negative value” (since, assuming that the entities involved are integers, x may end up being non-negative after the assignment, depending on the value of y). These examples illustrate the property that must serve as the starting point of any discussion of correctness: A software system or software element is neither correct nor incorrect per se; it is correct or incorrect with respect to a certain specification. Strictly speaking, we should not discuss whether software elements are correct, but whether they are consistent with their specifications. This discussion will continue to use the well-accepted term “correctness”, but we should always remember that the question of correctness does not apply to software elements; it applies to pairs made of a software element and a specification. Software Correctness property Correctness is a relative notion
334 DESIGN BY CONTRACT:BUILDING RELIABLE SOFTWARE $11.3 In this chapter we will learn how to express such specifications through assertions, to help us assess the correctness of our software.But we will go further.It turns out (and only someone who has not practiced the approach will think of this as a paradox)that just writing the specification is a precious first step towards ensuring that the software actually meets it.So we will derive tremendous benefits from writing the assertions at the same time as we write the software-or indeed before we write the software.Among the consequences we will find the following: Producing software that is correct from the start because it is designed to be correct.[Mills 1975]. The title of an article written by Harlan D.Mills (one of the originators of "Structured Programming")in the nineteen-seventies provides the right mood:How to write correct programs and know it.To"know it"means to equip the software,at the time you write it,with the arguments showing its correctness. Getting a much better understanding of the problem and its eventual solutions. Facilitating the task of software documentation.As we will see later in this chapter, assertions will play a central part in the object-oriented approach to documentation. Providing a basis for systematic testing and debugging. The rest of this chapter explores these applications. A word of warning:C,C++and some other languages(following the lead of Algol W)have an "assert"instruction that tests whether a certain condition holds at a certain stage of the software's execution,and stops execution if it does not.Although relevant to the present discussion,this concept represents only a small part of the use of assertions in the object-oriented method.So if like many other software developers you are familiar with such instructions but have not been exposed to the more general picture,almost all the concepts of this chapter will be new. 11.3 EXPRESSING A SPECIFICATION We can turn the preceding informal observations into a simple mathematical notation, borrowed from the theory of formal program validation,and precious for reasoning about the correctness of software elements. Correctness formulae Let A be some operation (for example an instruction or a routine body).A correctness formula is an expression of the form P)AO denoting the following property,which may or may not hold:
334 DESIGN BY CONTRACT: BUILDING RELIABLE SOFTWARE §11.3 In this chapter we will learn how to express such specifications through assertions, to help us assess the correctness of our software. But we will go further. It turns out (and only someone who has not practiced the approach will think of this as a paradox) that just writing the specification is a precious first step towards ensuring that the software actually meets it. So we will derive tremendous benefits from writing the assertions at the same time as we write the software — or indeed before we write the software. Among the consequences we will find the following: • Producing software that is correct from the start because it is designed to be correct. The title of an article written by Harlan D. Mills (one of the originators of “Structured Programming”) in the nineteen-seventies provides the right mood: How to write correct programs and know it. To “know it” means to equip the software, at the time you write it, with the arguments showing its correctness. • Getting a much better understanding of the problem and its eventual solutions. • Facilitating the task of software documentation. As we will see later in this chapter, assertions will play a central part in the object-oriented approach to documentation. • Providing a basis for systematic testing and debugging. The rest of this chapter explores these applications. A word of warning: C, C++ and some other languages (following the lead of Algol W) have an “assert” instruction that tests whether a certain condition holds at a certain stage of the software’s execution, and stops execution if it does not. Although relevant to the present discussion, this concept represents only a small part of the use of assertions in the object-oriented method. So if like many other software developers you are familiar with such instructions but have not been exposed to the more general picture, almost all the concepts of this chapter will be new. 11.3 EXPRESSING A SPECIFICATION We can turn the preceding informal observations into a simple mathematical notation, borrowed from the theory of formal program validation, and precious for reasoning about the correctness of software elements. Correctness formulae Let A be some operation (for example an instruction or a routine body). A correctness formula is an expression of the form denoting the following property, which may or may not hold: {P} A {Q} [Mills 1975]
$11.3 EXPRESSING A SPECIFICATION 335 Meaning of a correctness formulaP)AO) "Any execution of A,starting in a state where P holds,will terminate in a state where O holds." Correctness formulae (also called Hoare triples)are a mathematical notation,not a programming construct;they are not part of our software language,but only designed to guide us through this discussion by helping to express properties of software elements. In P)O)we have seen that A denotes an operation;P and O are properties of the various entities involved,also called assertions (the word will be defined more precisely later).Ofthe two assertions,P is called the precondition and Othe postcondition. Here is a trivial correctness formula (which,assuming that x is an integer entity,holds): {x>=9}x:=x+5{x>=13} The use of correctness formulae is a direct application of the Software Correctness Property.What the Property stated informally-that correctness is only meaningful relative to a particular specification-correctness formulae turn into a form that is directly usable for working on the software:from now on the discourse about software correctness will not be about individual software elements 4,but about triples containing a software element 4,a precondition P and a postcondition O.The sole aim of the game is to establish that the resulting P)4O)correctness formulae hold. The number /3 appearing in the postcondition is not a typo!Assuming a correct implementation of integer arithmetic,the above formula holds:ifx>=9 is true before the instruction,x>=/3 will be true after the instruction.Of course we can assert more interesting things:with the given precondition,the most interesting postcondition is the strongest possible one,herex>=/4;with the given postcondition,the most interesting precondition is the weakest possible one,herex>=8.From a formula that holds,you can always get another one by strengthening the precondition or weakening the postcondition We will now examine more carefully these notions of"stronger"and "weaker". Weak and strong conditions One way to look at a specification of the formP)A(O)is to view it as a job description for 4-an ad in the paper,which states "We are looking for someone whose work will be to start from initial situations as characterized by P,and deliver results as defined by O". Here is a small quiz to help you sharpen your understanding of the concepts. Assume one of your friends is looking for a job and comes across several such ads, all with similar salary and benefits,but differing by their Ps and Os.(Tough times have encouraged the companies that publish the ads to resort to this notation,which they like for its mathematical compactness since the newspaper charges by the word.)Like everyone else,your friend is lazy,that is to say,wants to have the easiest possible job.He is asking for your advice,always a dangerous situation.What should you recommend for P:choose a job with a weak precondition,or a strong one?Same question for the postcondition O.(The answers appear right after this,but do take the time to decide the issue for yourself before turning the page.)
§11.3 EXPRESSING A SPECIFICATION 335 Correctness formulae (also called Hoare triples) are a mathematical notation, not a programming construct; they are not part of our software language, but only designed to guide us through this discussion by helping to express properties of software elements. In {P} A {Q} we have seen that A denotes an operation; P and Q are properties of the various entities involved, also called assertions (the word will be defined more precisely later). Of the two assertions, P is called the precondition and Q the postcondition. Here is a trivial correctness formula (which, assuming that x is an integer entity, holds): The use of correctness formulae is a direct application of the Software Correctness Property. What the Property stated informally — that correctness is only meaningful relative to a particular specification — correctness formulae turn into a form that is directly usable for working on the software: from now on the discourse about software correctness will not be about individual software elements A, but about triples containing a software element A, a precondition P and a postcondition Q. The sole aim of the game is to establish that the resulting {P} A {Q} correctness formulae hold. The number 13 appearing in the postcondition is not a typo! Assuming a correct implementation of integer arithmetic, the above formula holds: if x >= 9 is true before the instruction, x >= 13 will be true after the instruction. Of course we can assert more interesting things: with the given precondition, the most interesting postcondition is the strongest possible one, here x >= 14; with the given postcondition, the most interesting precondition is the weakest possible one, here x >= 8. From a formula that holds, you can always get another one by strengthening the precondition or weakening the postcondition. We will now examine more carefully these notions of “stronger” and “weaker”. Weak and strong conditions One way to look at a specification of the form {P} A {Q} is to view it as a job description for A — an ad in the paper, which states “We are looking for someone whose work will be to start from initial situations as characterized by P, and deliver results as defined by Q”. Here is a small quiz to help you sharpen your understanding of the concepts. Assume one of your friends is looking for a job and comes across several such ads, all with similar salary and benefits, but differing by their Ps and Qs. (Tough times have encouraged the companies that publish the ads to resort to this notation, which they like for its mathematical compactness since the newspaper charges by the word.) Like everyone else, your friend is lazy, that is to say, wants to have the easiest possible job. He is asking for your advice, always a dangerous situation. What should you recommend for P: choose a job with a weak precondition, or a strong one? Same question for the postcondition Q. (The answers appear right after this, but do take the time to decide the issue for yourself before turning the page.) Meaning of a correctness formula {P} A {Q} “Any execution of A, starting in a state where P holds, will terminate in a state where Q holds.” {x >= 9} x := x + 5 {x >= 13}
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