3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 79
Текст из файла (страница 79)
The components x̄ and u of pairs (x̄, u) ∈ Ln × N correspond to the facts (i) and (ii)about the termination of AFIX explained in Step 1. Since Ln has the finitechain property, <lex is indeed well-founded on Ln × N. The bound functionranging over W is given byt ≡ (x̄, min {zℓ | 1 ≤ ℓ ≤ n ∧ x̄ ⊏ Fℓ [x̄]}).Compared with Example 12.7, the condition ℓ ∈ L is replaced here by “1 ≤ℓ ≤ n ∧ x̄ ⊏ Fℓ [x̄].”To establish premise (2′ ) of rule 39′ , we have to prove the correctnessformula{p ∧ B ∧ z̄ ≥ 0 ∧ ∃zi ≥ 0 : t[zj := zj + 1]j6=i = α}xi := Fi (x̄){t <lex α}for i ∈ {1, . . .
, n}. By the assignment axiom, it suffices to prove the implicationp ∧ B ∧ z̄ ≥ 0 ∧ ∃zi ≥ 0 : t[zj := zj + 1]j6=i = α→ t[xi := Fi (x̄)] <lex α.(12.31)We distinguish two cases.Case 1 x̄ ⊏ Fi [x̄].Then t[xi := Fi (x̄)] <lex α by the first component in the lexicographicalorder.Case 2 x̄ = Fi [x̄].Since B ≡ x̄ 6= F (x̄) holds, there exist indices ℓ ∈ {1, .
. . , n} withx̄ ⊏ Fℓ [x̄]. Moreover, ℓ 6= i for all such indices because x̄ = Fi [x̄]. Thusimplication (12.31) is equivalent top ∧ B ∧ z̄ ≥ 0 ∧ (x̄, min {zℓ + 1 | 1 ≤ ℓ ≤ n ∧ x̄ ⊏ Fℓ (x̄)}) = α→ (x̄, min {zℓ | 1 ≤ ℓ ≤ n ∧ x̄ ⊏ Fℓ (x̄)}) <lex α.So (x̄, min {zℓ | . . .}) <lex α by the second component in the lexicographical order.This proves (12.31) and hence premise (2′ ) of the fair repetition rule 39′ .Since premise (3′ ) of rule 39′ is clearly satisfied, we have proved|=fair {p} AFIX {p ∧ ¬B}.By the rule of consequence, we obtain the desired correctness result (12.29).45212 Fairness12.10 Exercises12.1. Prove the Input/Output Lemma 10.3 for nondeterministic programswith random assignments.12.2. Prove the Change and Access Lemma 10.4 for non- deterministic programs with random assignments.12.3.
Prove the Soundness of PNR and TNR Theorem 12.1.12.4. The instruction x :=? ≤ y which sets x to a value smaller or equal toy was proposed in Floyd [1967b].(i) Define the instruction’s semantics.(ii) Suggest an axiom for this instruction.(iii) Prove that for some nondeterministic program SMtot [[x :=? ≤ y]] = Mtot [[S]].12.5.
Prove that for no nondeterministic program SMtot [[x :=?]] = Mtot [[S]].Hint. Use the Bounded Nondeterminism Lemma 10.1.12.6. Formalize forward reasoning about random assignments by giving analternative axiom of the form {p} x :=? {. . .}.12.7. Consider the programS ≡ do x ≥ 0 → x := x − 1; y :=?⊓⊔ y ≥ 0 → y := y − 1od,where x and y are integer variables.(i) Prove termination of S by proving the correctness formula{true} S {true}in the system T N R.(ii) Explain why it is impossible to use an integer expression as a boundfunction in the termination proof of S.Hint.
Show that for a given initial state σ with σ(x) > 0 it is impossibleto predict the number of loop iterations in S.12.8. Give for the printer-user program PU1 considered in Example 12.4 a∗simplified transformed program Tfair(PU1) which uses only one schedulingvariable z, such that∗Mfair [[PU1]] = Mtot [[Tfair(PU1)]] mod {z}.12.10 Exercises45312.9.
Consider the premises (2) and (2′ ) of the fair repetition rules 39 and 39′ .Let z1 and z2 be integer variables. For which of the expressions t ≡ z1 + z2 ,t ≡ (z1 , z2 ) and t ≡ (z2 , z1 ) is the correctness formula{∃z1 ≥ 0 : t[z1 := z1 + 1] = α} skip {t < α}true? Depending on the form of t, the symbol < is interpreted as the usualordering on Z or as the lexicographic ordering on Z × Z.12.10. Consider the one-level nondeterministic programS ≡ do x > 0 → go := true⊓⊔ x > 0 → if go then x := x − 1; go := false fiod,where x is an integer variable and go is a Boolean variable.(i)(ii)(iii)(iv)(v)Show that S can diverge from any state σ with σ(x) > 0.Show that every fair computation of S is finite.Exhibit the transformed program Tfair (S).Show that every computation of Tfair (S) is fair.Prove the fair termination of S by proving the correctness formula{true} S {true}in the system FN.12.11.
Consider a run(E0 , i0 ). . .(Ej , ij ). . .of n components. We call it weakly fair if it satisfies the following condition:∞∞∀(1 ≤ i ≤ n) : ( ∀ j ∈ N : i ∈ Ej → ∃ j ∈ N : i = ij ).∞∞The quantifier ∀ is dual to ∃ and stands for “for all but finitely many.”(i) Define a weakly fair nondeterminism semantics Mwfair of one-level nondeterministic programs by analogy with Mfair . Prove that for all onelevel nondeterministic programs S and proper states σMfair [[S]](σ) ⊆ Mwfair [[S]](σ).(ii) Define a scheduler WFAIR as the scheduler FAIR but withUPDATE i ≡ zi :=?;for all j ∈ {1, .
. . , n} − {i} doif j ∈ E then zj := zj − 1 else zj :=? fiod.45412 FairnessDefine the notions of a weakly fair scheduler and of a universal weaklyfair scheduler by analogy with fair schedulers (see Definition 12.3). Provethat for n components WFAIR is a universal weakly fair scheduler.Hint. Modify the proof of the FAIR Scheduling Theorem 12.2.(iii) Define a transformation Twfair by analogy with the transformation Tfair .Prove that for every one-level nondeterministic program S and everyproper state σMwfair [[S]](σ) = Mtot [[Twfair (S)]](σ) mod Z,where Z is the set of scheduling variables zi used in Twfair .Hint. Modify the proof of the Embedding Theorem 12.3.(iv) Define the notion of weakly fair total correctness by analogy with fairtotal correctness.
Consider the following weakly fair repetition rule:(1) {p ∧ Bi } Si {p}, i ∈ {1, . . . , n},(2) {p ∧ Bi ∧ z̄ ≥ 0∧ ∃zi ≥ 0 : ∃ū ≥ 0 : t[if Bj then zj + 1 else uj fi]j6=i = α}Si{t < α}, i ∈ {1, . . . , n},(3) p ∧ z̄ ≥ 0 → t ∈ WVn{p} do ⊓⊔ni=1 Bi → Si od {p ∧ i=1 ¬Bi }where• u1 , . . ., un are integer variables that do not occur in p, t, Bi or Si , fori ∈ {1, . .
. , n},• ∃ū ≥ 0 abbreviates ∃u1 ≥ 0 : . . . : ∃un ≥ 0,and conditions (i)–(v) of the fair repetition rule 39 hold.Prove that the weakly fair repetition rule is sound for weakly fair totalcorrectness.Hint. Modify the proof of the Soundness of the Fair Repetition RuleTheorem 12.4.(v) Identify“print next line” ≡ skip.Prove{true} PU1 {true}in the sense of weakly fair total correctness using the weakly fair repetition rule. The program PU1 is defined in Section 12.1.12.11 Bibliographic Remarks45512.11 Bibliographic RemarksNondeterministic programs augmented by the random assignment are extensively studied in Apt and Plotkin [1986], where several related references canbe found.The verification method presented in this chapter is based on the transformational approach of Apt and Olderog [1983].
Different methods were proposed independently in Lehmann, Pnueli and Stavi [1981] and Grumberg,Francez, Makowsky and de Roever [1985].In all these papers fairness was studied only for one-level nondeterministicprograms. In Apt, Pnueli and Stavi [1984] the method of Apt and Olderog[1983] was generalized to arbitrary nondeterministic programs. Francez [1986]provides an extensive coverage of the subject including a presentation of thesemethods.We discussed here two versions of fairness —strong and weak. Some otherversions are discussed in Francez [1986].
More recently an alternative notion,called finitary fairness, was proposed by Alur and Henzinger [1994]. Finitaryfairness requires that for every run of a system there is an unknown but fixedbound k such that no enabled transition is postponed more than k consecutivetimes.Current work in this area has concentrated on the study of fairness for concurrent programs. Early references include Olderog and Apt [1988], wherethe transformational approach discussed here was extended to parallel programs and Back and Kurki-Suonio [1988] and Apt, Francez and Katz [1988],where fairness for distributed programs was studied. More recent referencesinclude Francez, Back and Kurki-Suonio [1992] and Joung [1996].In Olderog and Podelski [2009] it is investigated whether the approachof explicit fair scheduling also works with dynamic control, i.e., when newprocesses may be created dynamically. It is shown that the schedulers definedin Olderog and Apt [1988] carry over to weak fairness but not to strongfairness.The asynchronous fixpoint computation problem studied in Section 12.9has numerous applications, for example in logic programming, see Lassez andMaher [1984], and in constraint programming, see van Emden [1997].Appendix A SemanticsThe following transition axioms and rules were used in this book to definesemantics of the programming languages.(i) < skip, σ > → < E, σ >(ii) < u := t, σ > → < E, σ[u := σ(t)] >where u ∈ V ar is a simple variable or u ≡ a[s1 , .
. . , sn ], for a ∈ V ar.′(ii ) < x̄ := t̄, σ > → < E, σ[x̄ := σ(t̄)] >(iii)< S1 , σ > → < S 2 , τ >< S1 ; S, σ > → < S2 ; S, τ >(iv) < if B then S1 else S2 fi, σ > → < S1 , σ > where σ |= B.(v) < if B then S1 else S2 fi, σ > → < S2 , σ > where σ |= ¬B.(iv ′ ) < if B → S fi, σ > → < S, σ > where σ |= B.(v ′ ) < if B → S fi, σ > → < E, fail > where σ |= ¬B.(vi) < while B do S od, σ > → < S; while B do S od, σ >where σ |= B.(vii) < while B do S od, σ > → < E, σ > where σ |= ¬B.(viii) < P, σ > → < S, σ >, where P :: S ∈ D.(ix) < begin local x̄ := t̄; S end, σ > → < x̄ := t̄; S; x̄ := σ(x̄), σ >(x) < P (t̄), σ > → < begin local ū := t̄ end, σ >where P (ū) :: S ∈ D.(xi) < u := t, σ >→< E, σ[u := σ(t)] >where u is a (possibly subscripted) instance variable.(xii) < s.m, σ >→< begin local this := s; S end, σ >where σ(s) 6= null and m :: S ∈ D.457458A Semantics(xiii) < s.m, σ >→< E, fail > where σ(s) = null.(xiv) < s.m(t̄), σ >→< begin local this, ū := s, t̄; S end, σ >where σ(s) 6= null and m(ū) :: S ∈ D.(xv) < s.m(t̄), σ >→< E, fail > where σ(s) = null.(xvi) < u := new, σ >→< E, σ[u := new] >,where u is a (possibly subscripted) object variable.< Si , σ > → < T i , τ >(xvii)< [S1 k.
. .kSi k. . .kSn ], σ > → < [S1 k. . .kTi k. . .kSn ], τ >where i ∈ {1, . . . , n}< S, σ > →∗ < E, τ >(xviii)< hSi, σ > → < E, τ >< S, σ > →∗ < E, τ >(xix)where σ |= B.< await B then S end, σ > → < E, τ >(xx) < if ⊓⊔ni=1 Bi → Si fi, σ > → < Si , σ >where σ |= Bi and i ∈ {1, . . . , n}.Vn(xxi) < if ⊓⊔ni=1 Bi → Si fi, σ > → < E, fail > where σ |= i=1 ¬Bi .(xxii) < do ⊓⊔ni=1 Bi → Si od, σ > → < Si ; do ⊓⊔ni=1 Bi → Si od, σ >where σ |= Bi and i ∈ {1, .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
