3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 69
Текст из файла (страница 69)
Thus the distributed programs IIIrule 36 together with the rule of consequence yields the desired correctnessresult.⊓⊔SoundnessTo establish soundness of the above three proof systems we establish firstsoundness of the corresponding three proof rules for distributed programs.Theorem 11.2. (Distributed Programs I) The distributed programsrule 34 is sound for partial correctness.Proof. Assume that all premises of rule 34 are true in the sense of partialcorrectness.
By the soundness for partial correctness of the composition rule(rule 3) and of the rule of repetitive command (rule 31) we conclude|= {p} T (S) {I ∧ BLOCK}.(11.1)39411 Distributed ProgramsNowM[[S]]([[p]])={Sequentialization Theorem 11.1(i)}M[[T (S)]]([[p]]) ∩ [[TERM ]]⊆{(11.1)}[[I ∧ BLOCK]] ∩ [[TERM ]]⊆{[[I ∧ BLOCK]] ⊆ [[I]]}[[I ∧ TERM ]];that is,|= {p} S {I ∧ TERM }.⊓⊔This concludes the proof.Theorem 11.3. (Distributed Programs II) The distributed programs IIrule 35 is sound for weak total correctness.Proof. The proof is similar to that of the Distributed Programs I Theorem 11.2. Assume that all premises of rule 35 are true in the sense of totalcorrectness.
By an argument analogous to the one presented in the proof ofDistributed Programs I Theorem 11.2 we obtain|=tot {p} T (S) {I ∧ BLOCK}.(11.2)Also, since the premises of the distributed programs II rule 35 include allpremises of the distributed programs rule 34 and total correctness impliespartial correctness, we have by Distributed Programs I Theorem 11.2|= {p} S {I ∧ TERM }.(11.3)Suppose now that σ |= p. Then by (11.2) {⊥, fail}iMtot [[T (S)]](σ) = ∅; so bythe Sequentialization Theorem 11.1 (ii) {⊥, fail} ∩ Mwtot [[S]](σ) = ∅.
This inconjunction with (11.3) establishes|=wtot {p} S {I ∧ TERM },which concludes the proof.⊓⊔Finally, the soundness of the distributed programs III rule 36 is an immediate consequence of the following lemma. Here, as in Chapter 9, a programS is deadlock free relative to p if S cannot deadlock from any state σ for whichσ |= p.Lemma 11.4. (Deadlock Freedom) Assume that I is a global invariantrelative to p; that is, I satisfies premises (1) and (2) above in the sense11.4 Verification395of partial correctness, and assume that premise (5) holds as well; that is,I ∧ BLOCK → TERM .
Then S is deadlock free relative to p.Proof. As in the proof of the Distributed Programs I Theorem 11.2|= {p} T (S) {I ∧ BLOCK};so by the assumption and the soundness of the consequence rule|= {p} T (S) {TERM }.Thus,M[[T (S)]](σ) ⊆ [[TERM ]]for all σ such that σ |= p. Now by Sequentialization Theorem 11.1(iii) we getthe desired conclusion.⊓⊔We can now establish the desired result.Theorem 11.4.
(Distributed Programs III) The distributed programs IIIrule 36 is sound for total correctness.Proof. By the Distributed Programs II Theorem 11.3 and the DeadlockFreedom Lemma 11.4.⊓⊔The following theorem summarizes the above results.Theorem 11.5. (Soundness of PDP, WDP and TDP)(i) The proof system PDP is sound for partial correctness of distributedprograms.(ii) The proof system WDP is sound for weak total correctness of distributedprograms.(iii) The proof system TDP is sound for total correctness of distributed programs.Proof. See Exercise 11.6.⊓⊔A key to the proper understanding of the proof systems PDP, WDP andTDP studied in this chapter is the Sequentialization Theorem 11.1 relating adistributed program S to its transformed nondeterministic version T (S).
Thisconnection allows us to prove the correctness of S by studying the correctnessof T (S) instead, and the distributed program rules 34, 35 and 36 do just this—their premises refer to the subprograms of T (S) and not S.As we saw in Section 10.6, the same approach could be used when dealingwith parallel programs. However, there such a transformation of a parallelprogram into a nondeterministic program necessitates in general a use of39611 Distributed Programsauxiliary variables. This adds to the complexity of the proofs and makesthe approach clumsy and artificial.
Here, thanks to the special form of theprograms, the transformation turns out to be very simple and no auxiliaryvariables are needed. We can summarize this discussion by conceding thatthe proof method presented here exploits the particular form of the programsstudied.11.5 Case Study: A Transmission ProblemWe now wish to prove correctness of the distributed programTRANS ≡ [SENDERkFILTERkRECEIVER]solving the transmission problem of Example 11.2. Recall that the processSENDER is to transmit to the process RECEIVER through the processFILTER a sequence of M characters represented as a section a[0 : M ]of an array a of type integer → character.
We have M ≥ 1 anda 6∈ change(TRANS). For the transmission there is a channel input between SENDER and FILTER and a channel output between FILTER andRECEIVER.The task of FILTER is to delete all blanks ‘ ’ in the transmitted sequence.A special character ‘∗’ is used to mark the end of the sequence; that is, wehave a[M − 1] = ‘‘∗’′ . FILTER uses an array b of the same type as the arraya as an intermediate store. Upon termination of TRANS the result of thetransmission should be stored in the process RECEIVER in an array c of thesame type as the array a.The program TRANS is a typical example of a transmission problem wherethe process FILTER acts as an intermediary process between the processesSENDER and RECEIVER.We first formalize the correctness property we wish to prove about it.
Asa precondition we choosep ≡ M ≥ 1 ∧ a[M − 1] = ‘∗’ ∧ ∀(0 ≤ i < M − 1) : a[i] 6= ‘∗’.To formulate the postcondition we need a functiondelete : character∗ → character∗ ,where character∗ denotes the set of all strings over the alphabet character.This mapping is defined inductively as follows:• delete(ε) = ε,• delete(w.‘ ′ ) = delete(w),• delete(w.a) = delete(w).aif a 6= ‘ ’.11.5 Case Study: A Transmission Problem397Here ε denotes the empty string, w stands for an arbitary string over character and a for an arbitrary symbol from character.
The postcondition cannow be formulated asq ≡ c[0 : j − 1] = delete(a[0 : M − 1]).Our aim in this case study is to show|=tot {p} TRANS {q}.(11.4)We proceed in four steps.Step 1. Decomposing Total CorrectnessWe use the fact that a proof of total correctness of a distributed program canbe decomposed into proofs of• partial correctness,• absence of failures and of divergence,• deadlock freedom.Step 2.
Proving Partial CorrectnessWe first prove (11.4) in the sense of partial correctness; that is, we show|= {p} TRANS {q}.To this end we first need an appropriate global invariant I of TRANS relativeto p. We putI≡b[0 : in − 1] = delete(a[0 : i − 1])∧ b[0 : out − 1] = c[0 : j − 1]∧ out ≤ in.Here in and out are the integer variables used in the process FILTER to pointat elements of the array b. We now check that I indeed satisfies the premisesof the distributed programs rule 34. Recall that these premises refer to thetransformed nondeterministic version T (TRANS) of the program TRANS:T (TRANS) ≡ i := 0; in := 0; out := 0;x := ‘ ’; j := 0; y := ‘ ’;do i 6= M ∧ x 6= ‘∗’ → x := a[i]; i := i + 1;if x = ‘ ’ → skip⊓⊔ x 6= ‘ ’ → b[in] := x;39811 Distributed Programsin := in + 1fi⊓⊔ out 6= in ∧ y =6 ‘∗’ → y := b[out]; out := out + 1;c[j] := y; j := j + 1od.(a) First we consider the initialization part.
Clearly, we have{p}i := 0; in := 0; out := 0;x := ‘ ’; j := 0; y := ‘ ’{I}as by convention a[0 : −1], b[0 : −1] and c[0 : −1] denote empty strings.(b) Next we show that every communication along the channel input involvingthe matching i/o commands input!a[i] and input?x preserves the invariant I.The corresponding premise of the distributed programs rule 34 refers to thefirst part of the do loop in T (TRANS):{I ∧ i 6= M ∧ x 6= ‘∗’}x := a[i]; i := i + 1;if x = ‘ ’ → skip⊓⊔ x 6= ‘ ’ → b[in] := x;in := in + 1fi{I}.We begin with the first conjunct of I; that is, b[0 : in−1] = delete(a[0 : i−1]).By the definition of the mapping delete the correctness formulas{b[0 : in − 1] = delete(a[0 : i − 1])}x := a[i]; i := i + 1;{b[0 : in − 1] = delete(a[0 : i − 2]) ∧ a[i − 1] = x}and{b[0 : in − 1] = delete(a[0 : i − 2]) ∧ a[i − 1] = x ∧ x = ‘ ’}skip{b[0 : in − 1] = delete(a[0 : i − 1])}and{b[0 : in − 1] = delete(a[0 : i − 2]) ∧ a[i − 1] = x ∧ x 6= ‘ ’}b[in] := x; in := in + 1{b[0 : in − 1] = delete(a[0 : i − 1])}hold.
Thus the alternative command rule and the composition rule yield{b[0 : in − 1] = delete(a[0 : i − 1])}x := a[i]; i := i + 1;11.5 Case Study: A Transmission Problem399if x = ‘ ’ → skip⊓⊔x=6 ‘ ’ → b[in] := x;in := in + 1fi{b[0 : in − 1] = delete(a[0 : i − 1])}.Now we consider the last two conjuncts of I; that is,b[0 : out − 1] = c[0 : j − 1] ∧ out ≤ in.Since this assertion is disjoint from the program part considered here (theassignment b[in] := x does not modify the section b[0 : out−1]), we can applythe invariance rule A6 to deduce that I is preserved altogether.(c) Next we show that also every communication along the channel output involving the matching i/o commands output!b[out] and output?y preserves theinvariant I.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
