3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 76
Текст из файла (страница 76)
In the more complicated examples weuse proof outlines for fair total correctness. They are defined in the usual way,with reference to the premises of rule 39, when dealing with loop invariantsp and bound functions t.Example 12.5. Consider the printer-user programPU1 ≡ signal := false;do ¬signal → “print next line”⊓⊔ ¬signal → signal := trueodof Section 12.1. We wish to prove that PU1 terminates under the assumptionof fairness, that is,|=fair {true} PU1 {true}.Since printing a line does not change the variable signal, we identify“print next line” ≡ skip.Using the new proof system FN, we first prove{true}do ¬signal → skip⊓⊔ ¬signal → signal := trueod{signal}(12.8)with its fair repetition rule 39′ dealing with identical guards. Finding anappropriate loop invariant is trivial: we just takep ≡ true.More interesting is the choice of the bound function t.
We take the conditionalexpressiont ≡ if ¬signal then z2 + 1 else 0 fi.Here we use the scheduling variable z2 associated with the second componentof the do loop. Clearly, t ranges over the set Z of integers which, under theusual ordering <, is well-founded on the subsetW =Nof natural numbers.Intuitively, t counts the maximal number of rounds through the loop. Ifthe signal is true, the loop terminates, hence no round will be performed. Ifthe signal is false, z2 + 1 rounds will be performed: the scheduling variable43412 Fairnessz2 counts how many rounds the second component of the loop has neglectedand +1 counts the final round through the second component.Formally, we check the premises (1′ )-(3′ ) of the fair repetition rule 39′ .Premises (1′ ) and (3′ ) are obviously satisfied.
The interesting premise is (2′ )which deals with the decrease of the bound function.(a) For the first component of the do loop we have to prove{true ∧ ¬signal ∧ z1 ≥ 0 ∧ z2 ≥ 0∧ ∃z1 ≥ 0 : if ¬signal then z2 + 2 else 0 fi = α}skip{if ¬signal then z2 + 1 else 0 fi < α}(12.9)in the system FN. By the skip axiom 1 and the consequence rule 6, it sufficesto show that the precondition implies the postcondition. This amounts tochecking the implicationz2 + 2 = α → z2 + 1 < αwhich is clearly true.Thus, when the first component is executed, the scheduling variable z2 isresponsible for the decrease of the bound function t.(b) For the second component we have to prove{true ∧ ¬signal ∧ z1 ≥ 0 ∧ z2 ≥ 0∧ ∃z2 ≥ 0 : if ¬signal then z2 + 1 else 0 fi = α}signal := true{if ¬signal then z2 + 1 else 0 fi < α}(12.10)in FN.
By the assignment axiom 2 and the rule of consequence, it suffices toshow∃z2 ≥ 0 : z2 + 1 = α → 0 < α.Since ∃z2 ≥ 0 : z2 + 1 = α is equivalent to α ≥ 1, this implication is true.Thus, when the second component is executed, the program variable signalis responsible for the decrease of t.By (12.9) and (12.10), premise (2′ ) is proved in FN. Now an applicationof the fair repetition rule 39′ yields (12.8). Finally, (12.8) implies|=fair {true} PU1 {true},the desired termination result about PU1.⊓⊔12.7 Verification435Example 12.6. More complicated is the analysis of the modified printer-userprogramPU2 ≡ signal := false; full-page := false; ℓ := 0;do ¬signal → “print next line”;ℓ := (ℓ + 1) mod 30; printerfull-page := ℓ = 0o⊓⊔ ¬signal ∧ full-page → signal := true userodof Section 12.1.
We wish to prove that under the assumption of fairness PU2terminates in a state where the printer has received the signal of the user andcompleted its current page, that is,|=fair {true} PU2 {signal ∧ full-page}.A proof outline for fair total correctness in the system FN has the followingstructure:{true}signal := false;full-page := false;ℓ := 0;{¬signal ∧ ¬full-page ∧ ℓ = 0}{inv : p}{bd : t}do ¬signal → {p ∧ ¬signal}skip;ℓ := (ℓ + 1) mod 30;full-page := ℓ = 0{p}⊓⊔ ¬signal ∧ full-page → {p ∧ ¬signal ∧ full-page}signal := true{p}od{p ∧ signal ∧ (signal ∨ ¬full-page)}{signal ∧ full-page},where we again identify“print next line” ≡ skip.The crucial task now is finding an appropriate loop invariant p and an appropriate bound function t that satisfy the premises of the fair repetition rule 39and thus completing the proof outline.As an invariant we take the assertionp ≡ 0 ≤ ℓ ≤ 29 ∧ signal → full-page.43612 FairnessThe bounds for the variable ℓ appear because ℓ is incremented modulo 30.Since the implications¬signal ∧ ¬full-page ∧ ℓ = 0 → pandp ∧ signal → signal ∧ full-pageare true, p fits into the proof outline as given outside the do loop.
To checkthat p is kept invariant within the loop, we have to prove premise (1) ofthe fair repetition rule 39. This is easily done because the loop componentsconsist only of assignment statements.More difficult is the choice of a suitable bound function t. As in the previousexample PU1, the second component signal := true is responsible for the(fair) termination of the loop. But because of the different guards in the loop,the bound functiont ≡ if ¬signal then z2 + 1 else 0 fiused for PU1 is not sufficient any more to establish premise (2) of the fairrepetition rule 39.Indeed, for the first component we should prove{p ∧ ¬signal ∧ z1 ≥ 0 ∧ z2 ≥ 0∧ if full-page thenz2 + 2 else z2 + 1 fi = α}skip;ℓ := (ℓ + 1) mod 30; ≡ S1full-page := ℓ = 0{z2 + 1 < α},which is wrong if full-page is initially false.
In this case, however, the executionof the command S1 approaches a state where full-page is true. If ℓ drops from29 to 0, S1 sets full-page to true immediately. Otherwise S1 increments ℓ by1 so that ℓ gets closer to 29 with the subsequent drop to 0.Thus we observe here a hierarchy of changes:• a change of the variable ℓ indicates progress toward• a change of the variable full-page which (by fairness) indicates prog-resstoward• a selection of the second component that, by changing the variable signal,leads to termination of the loop.Proving termination of a loop with such a hierarchy of changes is bestdone by a bound function t ranging over a product P of structures orderedlexicographically by <lex (cf.
Section 12.4).Here we takeP = Z × Z × Z,12.7 Verification437which under <lex is well-founded on the subsetW = N × N × N,andt ≡ if ¬signal then (z2 + 1, int(full-page), 29 − ℓ)else (0, 0, 0) fi,where int(true) = 1 and int(false) = 0 (cf. Section 2.2). This definition oft reflects the intended hierarchy of changes: a change in the first component(variable z2 ) weighs more than a change in the second component (variablefull-page), which in turn weighs more than a change in the third component(variable ℓ).Now we can prove premise (2) of the fair repetition rule 39.
For the firstloop component we have the following proof outline:{p ∧ ¬signal ∧ z1 ≥ 0 ∧ z2 ≥ 0∧ if full-page then (z2 + 2, 0, 29 − ℓ)else (z2 + 1, 1, 29 − ℓ) fi = α}skip;{if ℓ < 29 then (z2 + 1, 1, 29 − ℓ − 1)else (z2 + 1, 0, 0) fi <lex α}ℓ := (ℓ + 1) mod 30;{(z2 + 1, int(¬(ℓ = 0)), 29 − ℓ) <lex α}full-page := ℓ = 0{(z2 + 1, int(¬full-page), 29 − ℓ) <lex α}.(12.11)(12.12)(12.13)(12.14)Obviously, the assertion (12.13) is obtained from (12.14) by performing thebackward substitution of the assignment axiom. To obtain assertion (12.12)from (12.13) we recalled the definition of “modulo 30”:ℓ := (ℓ + 1) mod 30abbreviatesℓ := ℓ + 1;if ℓ < 30 then skip else ℓ := 0 fi,and we applied the corresponding proof rules. Finally, by the skip axiom andthe rule of consequence, the step from assertion (12.11) to assertion (12.12)is proved if we show the following implication:if full-page then (z2 + 2, 0, 29 − ℓ)else (z2 + 1, 1, 29 − ℓ) fi = α→if ℓ < 29 then (z2 + 1, 1, 29 − ℓ − 1)else (z2 + 1, 0, 0) fi <lex α.We proceed by case analysis.43812 FairnessCase 1 full-page is true.Then the implication is justified by looking at the first component of α :z2 + 1 < z2 + 2.Case 2 full-page is false.If ℓ = 29, the implication is justified by the second component of α since0 < 1; if ℓ < 29, it is justified by the third component of α since 29 − ℓ − 1 <29 − ℓ.Compared with the first loop component dealing with the second loopcomponent is simpler: the correctness formula{p ∧ ¬signal ∧ full-page ∧ z1 ≥ 0 ∧ z2 ≥ 0∧ ∃z2 ≥ 0 : (z2 + 1, 0, 29 − ℓ) = α}signal := true{(0, 0, 0) <lex α}is true because the first component of α is ≥ 1.
This finishes the proof ofpremise (2) of the fair repetition rule 39.Since premise (3) of rule 39 is obviously true, we have now a completeproof outline for fair total correctness for the program PU2. Hence,|=fair {true} PU2 {signal ∧ full-page}as desired.⊓⊔SoundnessFinally, we prove soundness of the proof system F N . We concentrate here onthe soundness proof of the fair repetition rule.Theorem 12.4. (Soundness of the Fair Repetition Rule) The fair repetition rule 39 is sound for fair total correctness; that is, if its premises (1)–(3)are true in the sense of total correctness, then its conclusion (12.2) is truein the sense of fair total correctness.Proof. Let S ≡ do ⊓⊔ni=1 Bi → Si od.
By the Fairness Corollary 12.1,VnVn|=fair {p} S {p ∧ i=1 ¬Bi } iff |=tot {p} Tfair (S) {p ∧ i=1 ¬Bi }.Thus rule 39 is sound if the truth of its premises (1)–(3) implies the truth ofVn{p} Tfair (S) {p ∧ i=1 ¬Bi },all in the sense of total correctness.12.7 Verification439To show the latter, we establish three claims. In their proofs we repeatedlyuse the Soundness of PNR and TNR Theorem 12.1(ii), which states soundnessof the proof system TNR for total correctness of nondeterministic programswith random assignments.
Let INIT , SCH i and UPDATE i be the parts addedto S by Tfair and let INV be the standard invariant established for FAIR inthe proof of the Fair Scheduling Theorem 12.2:INV ≡n^card {i ∈ {1, . . . , n} | zi ≤ −k} ≤ n − k.k=1The first claim establishes this invariant for the loop in Tfair (S) by mergingthe invariants of FAIR and S.Claim 1 For i ∈ {1, . . . , n}|=tot {p ∧ Bi } Si {p}(12.15)implies|=tot {p ∧ INV ∧ Bi ∧ SCH i } UPDATE i ; Si {p ∧ INV }.(12.16)Proof of Claim 1. Since Si does not change z1 , . . ., zn , the free variables ofINV , (12.15) implies by the soundness of the invariance rule A6|=tot {p ∧ INV ∧ Bi } Si {p ∧ INV }.(12.17)By the proof of the Fair Scheduling Theorem 12.2, UPDATE i satisfies|=tot {INV ∧ SCH i } UPDATE i {INV }.(12.18)Since UPDATE i only changes the variables z1 , .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
