$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