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: