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,there336 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}