3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 77
Текст из файла (страница 77)
. ., zn and they are not free inp or Bi , (12.18) implies by the soundness of the invariance rule A6|=tot {p ∧ INV ∧ Bi ∧ SCH i } UPDATE i {p ∧ INV ∧ Bi }.(12.19)Now by the soundness of the composition rule, (12.19) and (12.17) imply(12.16).⊓⊔Define the expression t′ by the following substitution performed on t:t′ ≡ t[zi := zi + n]i∈{1, . . . , n} .This substitution represents a shift by n in the values of zi .
It allows us toconsider t in the following claim only for values zi ≥ 0 whereas t′ takes careof all the values that are possible for zi due to the invariant INV of thescheduler FAIR, namely zi ≥ −n.44012 FairnessClaim 2 For i ∈ {1, . . . , n}|=tot {p ∧ Bi ∧ z̄ ≥ 0∧ ∃zi ≥ 0 : t[zj := if Bj then zj + 1 else zj fi]j6=i = α}Si(12.20){t < α}implies|=tot {p ∧ INV ∧ Bi ∧ SCH i ∧ t′ = α}UPDATE i ; Si{t′ < α}.(12.21)Proof of Claim 2. Fix i ∈ {1, .
. . , n}. Since the variables z1 , . . ., zn are notfree in p, Bi or Si , substituting for j ∈ {1, . . . , n} the expression zj + n for zjin the pre- and postcondition of (12.20) yields:|=tot {p ∧ Bi ∧ z̄ ≥ −n∧ ∃zi ≥ −n : t′ [zj := if Bj then zj + 1 else zj fi]j6=i = α}Si(12.22){t′ < α}.We use here the abbreviationz̄ ≥ −n ≡ z1 ≥ −n ∧ .
. . ∧ zn ≥ −nand the definition of t′ . This explains the change in the range of the existentialquantifier over the bound variable zi .Next, by the truth of the axioms for ordinary and random assignments 2and 37 and the soundness of the conditional rule 4 and the consequence rule 6we get|=tot {zi ≥ −n ∧ t′ = α}UPDATE i(12.23){∃zi ≥ −n : t′ [zj := if Bj then zj + 1 else zj fi]j6=i = α}.INV implies zi ≥ −n, so combining (12.19), established in the proof of Claim1, and (12.23) yields by the soundness of the conjunction rule A4 and of theconsequence rule|=tot {p ∧ INV ∧ Bi ∧ SCH i ∧ t′ = α}UPDATE i(12.24){p ∧ INV ∧ Bi∧ ∃zi ≥ −n : t′ [zj := if Bj then zj + 1 else zj fi]j6=i = α}.Since INV implies z̄ ≥ −n, the postcondition of (12.24) impliesp ∧ Bi ∧ z̄ ≥ −n∧ ∃zi ≥ −n : t′ [zj := if Bj then zj + 1 else zj fi]j6=i = α,12.7 Verification441the precondition of (12.22).
Thus, by the soundness of the consequence ruleand the composition rule, (12.24) and (12.22) imply (12.21).⊓⊔Claim 3p ∧ z̄ ≥ 0 → t ∈ W(12.25)p ∧ INV → t′ ∈ W.(12.26)impliesProof of Claim 3. By the definition of INV , the implicationp ∧ INV → p ∧ z̄ + n ≥ 0holds, with z̄ + n ≥ 0 abbreviating z1 + n ≥ 0 ∧ . . . ∧ zn + n ≥ 0. Also,substituting everywhere in (12.25) the expression zi + n for zi , i ∈ {1, .
. . , n},yields:p ∧ z̄ + n ≥ 0 → t[zi := zi + n]i∈{1, . . . , n} ∈ W.Thus, by the definition of t′ , (12.26) follows.⊓⊔We now return to the main proof. By Claims 1–3, the truth of the premises(1)–(3) of the fair repetition rule 39 implies the truth of the following (correctness) formulas (in the sense of total correctness):{p ∧ INV ∧ Bi ∧ SCH i } UPDATE i ; Si {p ∧ INV },{p ∧ INV ∧ Bi ∧ SCH i ∧ t = α} UPDATE i ; Si {t′ < α}, i ∈ {1, . . . , n},p ∧ INV → t′ ∈ W .Also {p} INIT {p ∧ INV } is true, since z1 , . .
., zn do not appear in p. Thesoundness of the composition rule and the repetitive command III rule 38implies the truth ofVn{p} INIT ; do ⊓⊔ni=1 Bi ∧ SCH i → UPDATE i ; Si od {p ∧ i=1 ¬Bi },that is, the truth of{p} Tfair (S) {p ∧Vni=1¬Bi },all in the sense of total correctness. This concludes the proof of Theorem 12.4.⊓⊔Corollary 12.2. (Soundness of FN) The proof system FN is sound forfair total correctness of one-level nondeterministic programs.44212 Fairness12.8 Case Study: Zero SearchIn this section we study a nondeterministic solution to our introductory problem of zero search.
Recall from Section 1.1 that given a function f from integers to integers the problem is to write a program that finds a zero of fprovided such a zero exists.Here we consider the nondeterministic programZERO-N ≡ f ound := false; x := 0; y := 1;do ¬f ound → x := x + 1;f ound := f (x) = 0⊓⊔ ¬f ound → y := y − 1;f ound := f (y) = 0od.ZERO-N searches for a zero of f with the help of two subprograms: oneis searching for this zero by incrementing its test values (x := x + 1) and theother one by decrementing them (y := y − 1). The idea is that ZERO-N findsthe desired zero by activating these subprograms in a nondeterministic, butfair order.Summarizing, we wish to prove|=fair {∃u : f (u) = 0} S {f (x) = 0 ∨ f (y) = 0}.The correctness proof takes place in the new proof system FN and is dividedinto three steps.Step 1 We first show that ZERO-N works correctly if f has a positive zerou:|=fair {f (u) = 0 ∧ u > 0} ZERO-N {f (x) = 0 ∨ f (y) = 0}.A proof outline for fair total correctness has the following structure:{f (u) = 0 ∧ u > 0}f ound := false;x := 0;y := 1;{f (u) = 0 ∧ u > 0 ∧ ¬f ound ∧ x = 0 ∧ y = 1}{inv : p}{bd : t}do ¬f ound → {p ∧ ¬f ound}x := x + 1;f ound := f (x) = 0{p}⊓⊔ ¬f ound → {p ∧ ¬f ound}y := y − 1;f ound := f (y) = 0(12.27)12.8 Case Study: Zero Search443{p}od{p ∧ f ound}{f (x) = 0 ∨ f (y) = 0}.It remains to find a loop invariant p and a bound function t that will completethis outline.Since the variable u is left unchanged by the program ZERO-N, certainlyf (u) = 0 ∧ u > 0is an invariant.
But for the completion of the proof outline we need a strongerinvariant relating u to the program variables x and f ound. We take as anoverall invariantp ≡f (u) = 0 ∧ u > 0 ∧ x ≤ u∧ if f ound then f (x) = 0 ∨ f (y) = 0 else x < u fi.Notice that the implicationsf (u) = 0 ∧ u > 0 ∧ ¬f ound ∧ x = 0 ∧ y = 1 → pandp ∧ f ound → f (x) = 0 ∨ f (y) = 0are obviously true and thus confirm the proof outline as given outside the doloop.To check the proof outline inside the loop, we need an appropriate boundfunction.
We observe the following hierarchy of changes:• by the assumption of fairness, executing the second loop component bringsus closer to a switch to the first loop component,• executing the first loop component brings us closer to the desired zero uby incrementing the test value x by 1.Hence, we take as partial order the setP = Z × Z,ordered lexicographically by <lex and well-founded on the subsetW = N × N,and as bound functiont ≡ (u − x, z1 ).In t the scheduling variable z1 counts the number of executions of the secondloop component before the next switch to the first one, and u−x, the distancebetween the current test value x and the zero u, counts the remaining numberof executions of the first loop component.44412 FairnessWe now show that our choices of p and t complete the overall proof outlineas given inside the do loop.
To this end, we have to prove in system FN thepremises (1′ )–(3′ ) of the fair repetition rule 39′ .We begin with premise (1′ ). For the first loop component we have thefollowing proof outline:{p ∧ ¬f ound}{f (u) = 0 ∧ u > 0 ∧ x < u}x := x + 1{f (u) = 0 ∧ u > 0 ∧ x ≤ u}{f (u) = 0 ∧ u > 0 ∧ x ≤ u∧ if f (x) = 0 then f (x) = 0 else x < u fi}f ound := f (x) = 0{f (u) = 0 ∧ u > 0 ∧ x ≤ u∧ if f ound then f (x) = 0 else x < u fi}{p}.Clearly, all implications expressed by successive assertions in this proof outline are true.
The assignments are dealt with by backward substitution of theassignment axiom.This is also the case for the proof outline of the second loop component:{p ∧ ¬f ound}{f (u) = 0 ∧ u > 0 ∧ x < u}y := y + 1{f (u) = 0 ∧ u > 0 ∧ x < u}{f (u) = 0 ∧ u > 0 ∧ x < u ∧ f (y) = 0 → f (y) = 0}f ound := f (y) = 0{f (u) = 0 ∧ u > 0 ∧ x < u ∧ f ound → f (y) = 0}{f (u) = 0 ∧ u > 0 ∧ x ≤ u∧ if f ound then f (y) = 0 else x < u fi}{p}.We now turn to premise (2′ ) of rule 39′ . For the first loop component wehave the proof outline:{¬f ound ∧ f (u) = 0 ∧ u > 0 ∧ x < u∧ z1 ≥ 0 ∧ z2 ≥ 0 ∧ ∃z1 ≥ 0 : (u − x, z1 ) = α}{∃z1 ≥ 0 : (u − x, z1 ) = α}{(u − x − 1, z1 ) <lex α}x := x + 1;{(u − x, z1 ) <lex α}f ound := f (x) = 0{(u − x, z1 ) <lex α}{t <lex α}.Thus the bound function t drops below α because the program variable x isincremented in the direction of the zero u.12.8 Case Study: Zero Search445For the second loop component we have the proof outline:{¬f ound ∧ f (u) = 0 ∧ u > 0 ∧ x < u∧ z1 ≥ 0 ∧ z2 ≥ 0 ∧ (u − x, z1 + 1) = α}{(u − x, z1 + 1) = α}{(u − x, z1 ) <lex α}y := y − 1;f ound := f (y) = 0{(u − x, z1 ) <lex α}{t <lex α}.Notice that we can prove that the bound function t drops here below α onlywith the help of the scheduling variable z1 ; the assignments to the programvariables y and f ound do not affect t at all.Finally, premise (3′ ) of rule 39′ follows from the implicationsp ∧ z̄ ≥ 0 → x ≤ u ∧ z1 ≥ 0andx ≤ u ∧ z1 ≥ 0 → t ∈ W.This completes the proof of (12.27).Step 2 Next we assume that f has a zero u ≤ 0.
The claim now is|=fair {f (u) = 0 ∧ u ≤ 0} ZERO-N {f (x) = 0 ∨ f (y) = 0}.(12.28)Its proof is entirely symmetric to that of Step 1: instead of the first loopcomponent now the second one is responsible for finding the zero.In fact, as loop invariant we takep≡f (u) = 0 ∧ u ≤ 0 ∧ u ≤ y∧ if f ound then f (x) = 0 ∨ f (y) = 0 else u < y fiand as bound functiont ≡ (y − u, z2 ).The well-founded structure is as before:W = N × N.Step 3 We combine the results (12.27) and (12.28) of Step 1 and Step 2.Using the disjunction rule A3 and the rule of consequence, we obtain|=fair {f (u) = 0} ZERO-N {f (x) = 0 ∨ f (y) = 0}.A final application of the ∃-introduction rule A5 yields|=fair {∃u : f (u) = 0} ZERO-N {f (x) = 0 ∨ f (y) = 0},44612 Fairnessthe desired result about ZERO-N.12.9 Case Study: Asynchronous Fixed PointComputationIn this section we verify a nondeterministic program for computing fixedpoints.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
