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}