$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}