346 DESIGN BY CONTRACT:BUILDING RELIABLE SOFTWARE $11.6 Using filter ■■ modules External objects Input and validation modules Processing modules In obtaining information from the outside (communication paths shown in color)you cannot rely on preconditions.But part of the task of the input modules shown in grey in the middle of the figure is to guarantee that no information is passed further to the right- to the modules responsible for the system's actual computations-unless it satisfies the conditions required for correct processing.In this approach there will be ample use of assertions in the software-to-software communication paths represented by the black dotted lines on the right.The postconditions achieved by the routines of the input modules will have to match(or exceed,in the sense of"stronger"defined earlier)the preconditions imposed by the processing routines. The routines of the filter classes may be compared to security officers in,say,a large government laboratory.To meet experts from the laboratory and ask them technical questions,you must submit to screening procedures.But it is not the same person who checks your authorization level and answers the questions.The physicists,once you have been officially brought into their offices,assume you satisfy the preconditions;and you will not get much help from the guards on theoretical physics. Assertions are not control structures Another common misunderstanding,related to the one just discussed,is to think of assertions as control structures-as techniques to handle special cases.It should be clear by now that this is not their role.If you want to write a routine sgrt that will handle negative arguments a certain way,and non-negative arguments another way,a require clause is not what you need.Conditional instructions (if...then...else...)and related constructs to deal with various cases (such as Pascal's case ..of...or the inspect instruction of this book's notation)are perfectly appropriate for such purposes. Assertions are something else.They express correctness conditions.If sgrt has its precondition,a call for whichx<0 is not a special case:it is a bug,plain and simple. Assertion Violation rule (1) A run-time assertion violation is the manifestation of a bug in the software. "Bug"is not a very scientific word but is clear enough to anyone in software;we will look for more precise terminology in the next section.For the moment we can pursue the assertion violation rule further by noting a consequence of the contract view:
346 DESIGN BY CONTRACT: BUILDING RELIABLE SOFTWARE §11.6 In obtaining information from the outside (communication paths shown in color) you cannot rely on preconditions. But part of the task of the input modules shown in grey in the middle of the figure is to guarantee that no information is passed further to the right — to the modules responsible for the system’s actual computations — unless it satisfies the conditions required for correct processing. In this approach there will be ample use of assertions in the software-to-software communication paths represented by the black dotted lines on the right. The postconditions achieved by the routines of the input modules will have to match (or exceed, in the sense of “stronger” defined earlier) the preconditions imposed by the processing routines. The routines of the filter classes may be compared to security officers in, say, a large government laboratory. To meet experts from the laboratory and ask them technical questions, you must submit to screening procedures. But it is not the same person who checks your authorization level and answers the questions. The physicists, once you have been officially brought into their offices, assume you satisfy the preconditions; and you will not get much help from the guards on theoretical physics. Assertions are not control structures Another common misunderstanding, related to the one just discussed, is to think of assertions as control structures — as techniques to handle special cases. It should be clear by now that this is not their role. If you want to write a routine sqrt that will handle negative arguments a certain way, and non-negative arguments another way, a require clause is not what you need. Conditional instructions (if … then … else …) and related constructs to deal with various cases (such as Pascal’s case … of … or the inspect instruction of this book’s notation) are perfectly appropriate for such purposes. Assertions are something else. They express correctness conditions. If sqrt has its precondition, a call for which x < 0 is not a special case: it is a bug, plain and simple. “Bug” is not a very scientific word but is clear enough to anyone in software; we will look for more precise terminology in the next section. For the moment we can pursue the assertion violation rule further by noting a consequence of the contract view: Assertion Violation rule (1) A run-time assertion violation is the manifestation of a bug in the software. External objects Input and validation modules Processing modules Using filter modules
$11.6 CONTRACTING FOR SOFTWARE RELIABILITY 347 Assertion violation rule(2) A precondition violation is the manifestation of a bug in the client. A postcondition violation is the manifestation of a bug in the supplier. A precondition violation means that the routine's caller,although obligated by the contract to satisfy a certain requirement,did not.This is a bug in the client itself the routine is not involved.("The customer is wrong".)An outside observer might of course criticize the contract as too demanding,as with the unsatisfiable require False precondition or our fictitious Sinecure example ("the customer is ahays wrong"),but this is too late to argue over the contract:it is the contract,and the client did not observe its part of the deal.So if there is a mechanism for monitoring assertions during execution -as will be introduced shortly-and it detects such a precondition violation,the routine should not be executed at all.It has stated the conditions under which it can operate,and these conditions do not hold;trying to execute it would make no sense. A postcondition violation means that the routine,presumably called under correct conditions,was not able to fulfill its contract.Here too the distribution of guilt and innocence is clear,although it is the reverse of the previous one:the bug is in the routine; the caller is innocent. Errors,defects and other creeping creatures The appearance of the word"bug"in the preceding analysis of assertion violation causes is a good opportunity to clarify the terminology.In Edsger W.Dijkstra's view,using the word"bug"is a lame attempt by software people to blame someone else by implying that mistakes somehow creep into the software from the outside while the developers are looking elsewhere-as if were not the developers who made the mistakes in the first place. Yet the term enjoys enduring success,if only because it is colorful and readily understood.Like the rest of the software literature,this book uses it freely.But it is appropriate to complement it by more specific(if more stodgy)terms for cases in which we need precise distinctions. Terms to denote software woes An error is a wrong decision made during the development of a software system. A defect is a property of a software system that may cause the system to depart from its intended behavior. A fault is the event of a software system departing from its intended behavior during one of its executions. The causal relation is clear:faults are due to defects,which result from errors
§11.6 CONTRACTING FOR SOFTWARE RELIABILITY 347 A precondition violation means that the routine’s caller, although obligated by the contract to satisfy a certain requirement, did not. This is a bug in the client itself; the routine is not involved. (“The customer is wrong”.) An outside observer might of course criticize the contract as too demanding, as with the unsatisfiable require False precondition or our fictitious Sinecure 1 example (“the customer is always wrong”), but this is too late to argue over the contract: it is the contract, and the client did not observe its part of the deal. So if there is a mechanism for monitoring assertions during execution — as will be introduced shortly — and it detects such a precondition violation, the routine should not be executed at all. It has stated the conditions under which it can operate, and these conditions do not hold; trying to execute it would make no sense. A postcondition violation means that the routine, presumably called under correct conditions, was not able to fulfill its contract. Here too the distribution of guilt and innocence is clear, although it is the reverse of the previous one: the bug is in the routine; the caller is innocent. Errors, defects and other creeping creatures The appearance of the word “bug” in the preceding analysis of assertion violation causes is a good opportunity to clarify the terminology. In Edsger W. Dijkstra’s view, using the word “bug” is a lame attempt by software people to blame someone else by implying that mistakes somehow creep into the software from the outside while the developers are looking elsewhere — as if were not the developers who made the mistakes in the first place. Yet the term enjoys enduring success, if only because it is colorful and readily understood. Like the rest of the software literature, this book uses it freely. But it is appropriate to complement it by more specific (if more stodgy) terms for cases in which we need precise distinctions. The causal relation is clear: faults are due to defects, which result from errors. Assertion violation rule (2) A precondition violation is the manifestation of a bug in the client. A postcondition violation is the manifestation of a bug in the supplier. Terms to denote software woes An error is a wrong decision made during the development of a software system. A defect is a property of a software system that may cause the system to depart from its intended behavior. A fault is the event of a software system departing from its intended behavior during one of its executions
348 DESIGN BY CONTRACT:BUILDING RELIABLE SOFTWARE $11.7 "Bug"usually has the meaning of defect ("are you sure there remains no other bug in this routine?").This is the interpretation in this book.But in informal discussions it is also used in the sense of fault("We have had bug-free operation for the last three weeks") or error ("the bug was that I used an unsorted list"). 11.7 WORKING WITH ASSERTIONS Let us now probe further the use of preconditions and postconditions,continuing with fairly elementary examples.Assertions,some simple,some elaborate,will be pervasive in the examples of the following chapters. A stack class The assertion-equipped ST4CK class was left in a sketchy form(STACK/).We can now come up with a full version including a spelled out implementation. For an effective (directly usable)class we must choose an implementation.Let us use the array implementation illustrated at the beginning of the discussion ofabstract data types: capacity “Push”operation: Stack count :count +I implemented representation (count]:=x with an array count (see page 123 (ARRAY_UP) for other representations) representation The array will be called representation and will have bounds I and capacity;the implementation also uses an integer,the attribute count,to mark the top of the stack Note that as we discover inheritance we will see how to write deferred classes that Foranara-based cover several possible implementations rather than just one.Even for a class that uses a stack implementation particular implementation,for example by arrays as here,we will be able to inherit from using inheritance,see “IMPLEMENTA- the implementation class ARRAY rather than use it as a client (although some object- TION INHERIT- oriented developers will still prefer the clientapproach).For the moment,however,we can ANCE”,24.8,page do without any inheritance-related technique. 844. Here is the class.Recall that if a is an array then the operation to assign value x to its i-th element is a.put (x,i),and the value of its i-th element is given by a.item (i)or, equivalently,a@i.If,as here,the bounds of the array are 1 and capacity,then i must in all cases lie between these bounds
348 DESIGN BY CONTRACT: BUILDING RELIABLE SOFTWARE §11.7 “Bug” usually has the meaning of defect (“are you sure there remains no other bug in this routine?”). This is the interpretation in this book. But in informal discussions it is also used in the sense of fault (“We have had bug-free operation for the last three weeks”) or error (“the bug was that I used an unsorted list”). 11.7 WORKING WITH ASSERTIONS Let us now probe further the use of preconditions and postconditions, continuing with fairly elementary examples. Assertions, some simple, some elaborate, will be pervasive in the examples of the following chapters. A stack class The assertion-equipped STACK class was left in a sketchy form (STACK1). We can now come up with a full version including a spelled out implementation. For an effective (directly usable) class we must choose an implementation. Let us use the array implementation illustrated at the beginning of the discussion of abstract data types: The array will be called representation and will have bounds 1 and capacity; the implementation also uses an integer, the attribute count, to mark the top of the stack. Note that as we discover inheritance we will see how to write deferred classes that cover several possible implementations rather than just one. Even for a class that uses a particular implementation, for example by arrays as here, we will be able to inherit from the implementation class ARRAY rather than use it as a client (although some objectoriented developers will still prefer the client approach). For the moment, however, we can do without any inheritance-related technique. Here is the class. Recall that if a is an array then the operation to assign value x to its i-th element is a ● put (x, i), and the value of its i-th element is given by a ● item (i) or, equivalently, a @ i. If, as here, the bounds of the array are 1 and capacity, then i must in all cases lie between these bounds. Stack implemented with an array (see page 123 for other representations) representation (ARRAY_UP) “Push” operation: count := count + 1 representation [count] := x count capacity 1 For an array-based stack implementation using inheritance, see “IMPLEMENTATION INHERITANCE”, 24.8, page 844
$11.7 WORKING WITH ASSERTIONS 349 indexing description:"Stacks:Dispenser structures with a Last-In,First-Out %access policy,and a fixed maximum capacity" class STACK2 [G]creation make feature -Initialization make (n:INTEGER)is --Allocate stack for a maximum of n elements require positive capacity:n>=0 do capacity :=n !representation.make (1,capacity) ensure capacity set:capacity =n array_allocated:representation /Void stack empty:empty end feature--Access On the export status capacity:INTEGER of capacity see exer- --Maximum number of stack elements cise E11.4.page 410. count:INTEGER --Number of stack elements item:G is --Top element require not empty:not empty--i.e.count>0 do Result representation count end feature--Status report empty:BOOLEAN is --Is stack empty? do Result:=(count ( ensure empty definition:Result (count =0) end
§11.7 WORKING WITH ASSERTIONS 349 indexing description: "Stacks: Dispenser structures with a Last-In, First-Out % %access policy, and a fixed maximum capacity" class STACK2 [G] creation make feature -- Initialization make (n: INTEGER) is -- Allocate stack for a maximum of n elements require positive_capacity: n >= 0 do capacity := n !! representation ● make (1, capacity) ensure capacity_set: capacity = n array_allocated: representation /= Void stack_empty: empty end feature -- Access capacity: INTEGER -- Maximum number of stack elements count: INTEGER -- Number of stack elements item: G is -- Top element require not_empty: not empty -- i.e. count > 0 do Result := representation @ count end feature -- Status report empty: BOOLEAN is -- Is stack empty? do Result := (count = 0) ensure empty_definition: Result = (count = 0) end On the export status of capacity see exercise E11.4, page 410
350 DESIGN BY CONTRACT:BUILDING RELIABLE SOFTWARE $11.7 full:BOOLEAN is -Is stack full? do Result (count capacity) ensure full definition:Result (count capacity) end feature--Element change put (x:G)is -Add x on top require not full:not full --i.e.count capacity in this representation do count :count I representation.put (count,x) ensure not empty:not empty added to top:item=x one_more item:count old count +I in top array entry:representation count =x end remove is --Remove top element require not empty:not empty --i.e.count >0 do count :count-1 ensure not full:not full one fewer:count old count-I end feature (NONE)--Implementation representation:ARRAY [G] --The array used to hold the stack elements invariant ..To be filled in later (see page 365)... end -class STACK2 Inyariants are This class text illustrates the simplicity of working with assertions.It is complete introduced in except for the invariant clause,which will be added later in this chapter.Let us explore "CLASS INVARI- its various properties. ANTS".11.8,page 364
350 DESIGN BY CONTRACT: BUILDING RELIABLE SOFTWARE §11.7 full: BOOLEAN is -- Is stack full? do Result := (count = capacity) ensure full_definition: Result = (count = capacity) end feature -- Element change put (x: G) is -- Add x on top require not_full: not full -- i.e. count < capacity in this representation do count := count + 1 representation ● put (count, x) ensure not_empty: not empty added_to_top: item = x one_more_item: count = old count + 1 in_top_array_entry: representation @ count = x end remove is -- Remove top element require not_empty: not empty -- i.e. count > 0 do count := count – 1 ensure not_full: not full one_fewer: count = old count – 1 end feature {NONE} -- Implementation representation: ARRAY [G] -- The array used to hold the stack elements invariant … To be filled in later (see page 365) … end -- class STACK2 This class text illustrates the simplicity of working with assertions. It is complete except for the invariant clause, which will be added later in this chapter. Let us explore its various properties. Invariants are introduced in “CLASS INVARIANTS”, 11.8, page 364