3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 75
Текст из файла (страница 75)
. . , n} for which Bk holds:E = {k | 1 ≤ k ≤ n ∧ Bk }.We see that the interaction between the program S and the scheduler FAIRtakes place in the guards of the do loop in Tfair (S). The guard of the ithcomponent can be passed only if it is enabled and selected by FAIR; that is,when both Bi and SCH i evaluate to true.42812 FairnessExpanding the abbreviations INIT , SCH i and UPDATE i from FAIRyields:Tfair (S) ≡ S0 ; z1 :=?; . . .; zn :=?;do ⊓⊔ni=1 Bi ∧ zi = min {zk | 1 ≤ k ≤ n ∧ Bk } →zi :=?;for all j ∈ {1, . . . , n} − {i} doif Bj then zj := zj − 1 fiod;Siod.In case of identical guards B1 ≡ .
. . ≡ Bn the transformation simplifies toTfair (S) ≡ S0 ; z1 :=?; . . .; zn :=?;do ⊓⊔ni=1 Bi ∧ zi = min {z1 , . . ., zn } →zi :=?;for all j ∈ {1, . . . , n} − {i} dozj := zj − 1od;Siod.In both cases we assume that the variables z1 , . . ., zn do not occur in S.Example 12.4. The printer-user programPU1 ≡ signal := false;do ¬signal → “print next line”⊓⊔ ¬signal → signal := trueoddiscussed in Section 12.1 is transformed intoTfair (PU1) ≡ signal := false; z1 :=?; z2 :=?;do ¬signal ∧ z1 ≤ z2 → z1 :=?; z2 := z2 − 1;“print next line”⊓⊔ ¬signal ∧ z2 ≤ z1 → z2 :=?; z1 := z1 − 1;signal := trueod.Note that in Tfair (PU1) it is impossible to activate exclusively the firstcomponent of the do loop because in every round through the loop the variable z2 gets decremented.
Thus eventually the conjunctz1 ≤ z2of the first guard will be falsified, but then the second guard with the conjunct12.6 Transformation429z2 ≤ z1will be enabled. Thus the second component of the do loop is eventuallyactivated. This leads to termination of Tfair (PU1).Thus for PU1 the aim of our transformation Tfair is achieved: with the helpof the scheduling variables z1 and z2 , the transformed program Tfair (PU1)generates exactly the fair computations of the original program PU1.⊓⊔But what is the semantic relationship between S and Tfair (S) in general?Due to the presence of the scheduling variables z1 , .
. ., zn in Tfair (S), the bestwe can prove is that the semantics Mfair [[S]] and Mtot [[Tfair (S)]] agree moduloz1 , . . ., zn ; that is, the final states agree on all variables except z1 , . . ., zn . Toexpress this we use the mod notation introduced in Section 2.3.Theorem 12.3. (Embedding) For every one-level nondeterministic program S and every proper state σMfair [[S]](σ) = Mtot [[Tfair (S)]](σ) mod Z,where Z is the set of scheduling variables zi used in Tfair .Proof. Let us call two computations Z-equivalent if they start in the samestate and either both diverge or both terminate in states that agree moduloZ.We prove the following two claims:(i) every computation of Tfair (S) is Z-equivalent to a fair computation ofS,(ii) every fair computation of S is Z-equivalent to a computation of Tfair (S).To this end, we relate the computations of Tfair (S) and S more intimately.A computation ξ ∗ of Tfair (S) is called an extension of a computation ξ of S tothe variables of Z if ξ ∗ results from ξ by adding transitions dealing exclusivelywith the variables in Z and by assigning in each state of ξ ∗ appropriate valuesto the variables in Z.
Conversely, a computation ξ of S is called a restrictionof a computation ξ ∗ of Tfair (S) to the variables in Z if all transitions referringto the variables in Z are deleted and the values of the variables in Z are resetin all states of ξ to the values in the first state of ξ ∗ .Observe the following equivalences:iffiffξ is a fair computation of S{definition of fairness}ξ is a computation of S with a fair run{Theorem 12.2}ξ is a computation of S with a run thatcan be checked by the scheduler FAIR.By these equivalences and the construction of Tfair , we conclude now:43012 Fairness(i) If ξ is a fair computation of S, there exists an extension ξ ∗ of ξ to thevariables in Z which is a computation of Tfair (S).(ii) If ξ ∗ is a computation of Tfair (S), the restriction ξ of ξ ∗ to the variablesin Z is a prefix of a fair computation of S.
We say “prefix” because itis conceivable that ξ ∗ exits the loop in Tfair (S) due to the additionalcondition SCH i in the guards, whereas S could continue looping andthus yield a longer computation than ξ. Fortunately, these prematureloop exits cannot happen because the scheduling relation of FAIR istotal (cf. Definition 12.2).
Thus if some guard Bi of S evaluates to true,one of the extended guards Bi ∧ SCH i of Tfair (S) will also evaluate totrue. Hence the above restriction ξ of ξ ∗ is really a fair computation ofS.Clearly, if ξ ∗ is an extension of ξ or ξ is a restriction of ξ ∗ , then ξ and ξ ∗ areZ-equivalent. Thus, (i′ ) and (ii′ ) imply (i) and (ii), establishing the claim ofthe theorem.⊓⊔12.7 VerificationTotal CorrectnessThe semantics Mfair induces the following notion of program correctness: acorrectness formula {p} S {q} is true in the sense of fair total correctness,abbreviated|=fair {p} S {q},ifMfair [[S]]([[p]]) ⊆ [[q]].The transformation Tfair enables us to develop a proof system for fair totalcorrectness. The starting point is the following corollary of the EmbeddingTheorem 12.3.Corollary 12.1.
(Fairness) Let p and q be assertions that do not containz1 , . . ., zn as free variables and let S be a one-level nondeterministic program.Then⊓⊔|=fair {p} S {q} iff |=tot {p} Tfair (S) {q}.Thus, in order to prove fair total correctness of S, it suffices to prove totalcorrectness of Tfair (S).
This suggests the proof rule{p} Tfair (S) {q}{p} S {q}12.7 Verification431for fair total correctness. Its premise has to be established in the proof system TNR for total correctness of nondeterministic programs with randomassignments introduced in Section 12.4.But, in fact, we can do slightly better by “absorbing” the parts INIT ,SCH i and UPDATE i added to S by Tfair into the assertions p and q. Thisprocess of absorption yields a new proof rule for fair repetition which in itspremise deals with the original one-level nondeterministic program S andwhich uses the scheduling variables z1 , . .
., zn of Tfair (S) only in the assertions. Thus Tfair allows us to derive and justify this new rule.RULE 39: FAIR REPETITIONwhere(1) {p ∧ Bi } Si {p}, i ∈ {1, . . . , n},(2) {p ∧ Bi ∧ z̄ ≥ 0∧ ∃zi ≥ 0 : t[zj := if Bj then zj + 1 else zj fi]j6=i = α}Si{t < α}, i ∈ {1, . . . , n},(3) p ∧ z̄ ≥ 0 → t ∈ WVn(4) {p} do ⊓⊔ni=1 Bi → Si od {p ∧ i=1 ¬Bi }(i) t is an expression which takes values in an irreflexive partial order (P, <)that is well-founded on the subset W ⊆ P ,(ii) z1 , .
. ., zn are integer variables that do not occur in p, Bi or Si , fori ∈ {1, . . . , n},(iii) t[zj := if Bj then zj + 1 else zj fi]j6=i denotes the expression that results from t by substituting for every occurrence of zj in t the conditional expression if Bj then zj + 1 else zj fi; here j ranges over the set{1, . . ., n} −{i},(iv) z̄ ≥ 0 abbreviates z1 ≥ 0 ∧ . . . ∧ zn ≥ 0,(v) α is a simple variable ranging over P and not occurring in p, t, Bi or Si ,for i ∈ {1, . .
. , n}.For identical guards B1 ≡ . . . ≡ Bn ≡ B this rule can be simplified. Inparticular, the substitutiont[zj := if Bj then zj + 1 else zj fi]j6=iin premise (2) simplifies tot[zj := zj + 1]j6=ibecause for each j the condition Bj ≡ Bi evaluates to true. This yields thefollowing specialization of the fair repetition rule 39.43212 FairnessRULE 39′ : FAIR REPETITION (IDENTICAL GUARDS)(1′ ) {p ∧ B} Si {p}, i ∈ {1, . . . , n},(2′ ) {p ∧ B ∧ z̄ ≥ 0 ∧ ∃zi ≥ 0 : t[zj := zj + 1]j6=i = α}Si{t < α}, i ∈ {1, . .
. , n},(3′ ) p ∧ z̄ ≥ 0 → t ∈ W(4′ ) {p} do ⊓⊔ni=1 B → Si od {p ∧ ¬B}where conditions analogous to (i)–(v) hold.Except for the additional variables z1 , . . ., zn the fair repetition rules 39and 39′ follow the pattern of the usual rule for total correctness of repetitivecommands in the system TNR (rule 38). Premise (1) of rule 39 establishespartial correctness of the do loop by showing that p is a loop invariant.Premise (2) of rule 39 establishes that t is a bound function of the loop, butwith the variables z1 , . . ., zn as “helpful ingredients.”Let us explain this point for the simplified fair repetition rule 39′ . Thevariables z1 , .
. ., zn may occur only in the expression t. In the precondition of(2′ ) the value zj + 1 instead of zj appears in t for all indices j 6= i. Amongother things this precondition states that for some value of zit[zj := zj + 1]j6=i = α.In the postcondition of (2′ ) we have to show thatt < α.Obviously, decrementing zj + 1 to zj is “helpful” for establishing that t hasdropped below α. On the other hand, the value of zi is not helpful for calculating the value of t because in the precondition of (2′ ) it is under the scopeof an existential quantifier.As we see in the subsequent soundness proof of the fair repetition rule 39,the precondition of premise (2) results from calculating the postcondition ofthe UPDATE i part in the transformation Tfair .We prove f air total correctness of one-level nondeterministic programsusing the following proof system FN.PROOF SYSTEM FN :This system is obtained from the proof system TNby replacing rule 33 by rule 39.Notice that the random assignment axiom 37 is not included in FN; thisaxiom is needed only to prove the soundness of the fair repetition rule 39.12.7 Verification433Let us demonstrate the power of the system FN, in particular that ofrule 39 (and 39′ ), by a few examples.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
