3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 27
Текст из файла (страница 27)
. , {pn } Pn {qn } ⊢ {p} S {q}1404 Recursive Programsimplies{p1 } P1 {q1 }, . . . , {pn } Pn {qn } |= {p} S {q}.⊓⊔Proof. See Exercise 4.5.Theorem 4.2. (Soundness of the Recursion Rule)Assume that D = P1 :: S1 , . . . , Pn :: Sn . Suppose that{p1 } P1 {q1 }, . . . , {pn } Pn {qn } ⊢ {p} S {q}and for i = 1, . . . , n{p1 } P1 {q1 }, . . . , {pn } Pn {qn } ⊢ {pi } Si {qi }.Then|= {p} S {q}.Proof. By the Soundness Theorem 4.1, we have{p1 } P1 {q1 }, . . . , {pn } Pn {qn } |= {p} S {q}(4.4)and for i = 1, .
. . , n{p1 } P1 {q1 }, . . . , {pn } Pn {qn } |= {pi } Si {qi }.(4.5)We first show that|= {pi } Pi {qi }(4.6)for i = 1, . . . , n. In the proof, as in the Input/Output Lemma 4.1, we referto different sets of procedure declarations and write D | S when we mean Sin the context of the set D of procedure declarations.
By the Input/OutputLemma 4.1(i) and (iii) we haveM[[D | Pi ]] =∞[k=0M[[Pik ]] = M[[Pi0 ]] ∪∞[M[[Dk | Pi ]] =k=0∞[M[[Dk | Pi ]],k=0so|= {pi } D | Pi {qi } iff for all k ≥ 0 we have |= {pi } Dk | Pi {qi }.We now prove by induction on k that for all k ≥ 0|= {pi } Dk | Pi {qi },for i = 1, . . . , n.Induction basis: k = 0. Since Si0 = Ω, by definition |= {pi } D0 | Pi {qi }holds, for i = 1, . . . , n.4.3 Verification141Induction step: k → k + 1. By the induction hypothesis, we have|= {pi } Dk | Pi {qi }, for i = 1, .
. . , n. Fix some i ∈ {1, . . ., n}. By (4.5),we obtain |= {pi } Dk | Si {qi }. By the Input/Output Lemma 4.1(i) and (ii),M[[Dk | Si ]] = M[[Sik+1 ]] = M[[Dk+1 | Sik+1 ]] = M[[Dk+1 | Pi ]],hence |= {pi } Dk+1 | Pi {qi }.This proves (4.6) for i = 1, . . . , n. Now (4.4) and (4.6) imply |= {p} S {q}(where we refer to the set D of procedure declarations).⊓⊔With this theorem we can state the following soundness result.Corollary 4.1. (Soundness of PR) The proof system PR is sound for partial correctness of recursive programs.Proof. The proof combines Theorem 4.2 with Theorem 3.1(i) on soundnessof the proof system PW and Theorem 3.7(i),(ii) on soundness of the auxiliaryrules.⊓⊔Next, we establish soundness of the recursion II rule and as a consequencethat of the proof system TR in the sense of total correctness.
Below we write{p1 } P1 {q1 }, . . . , {pn } Pn {qn } |=tot {p} S {q}when the following holds:for all sets of procedure declarations Dif |=tot {pi } Pi {qi }, for i = 1, . . . , n then |=tot {p} S {q}.As in the case of partial correctness we need a strengthening of the Soundness Theorem 3.1(ii). Recall that in this section the provability sign ⊢ refersto the proof system for total correctness that consists of the proof system TWextended by the auxiliary axioms and proof rules introduced in Section 3.8.Theorem 4.3.
(Soundness of Proofs from Assumptions){p1 } P1 {q1 }, . . . , {pn } Pn {qn } ⊢ {p} S {q}implies{p1 } P1 {q1 }, . . . , {pn } Pn {qn } |=tot {p} S {q}.Proof. See Exercise 4.6.⊓⊔Additionally, we shall need the following lemma that clarifies the reasonfor the qualification that the integer variable z is used as a constant.1424 Recursive ProgramsTheorem 4.4.
(Instantiation) Suppose that the integer variable z does notappear in S and in the proof{p1 } P1 {q1 }, . . . , {pn } Pn {qn } ⊢ {p} S {q}it is treated as a constant, that is, neither the ∃-introduction rule nor thesubstitution rule of Section 3.8 is applied to z. Then for all integers m{p1 θ} P1 {q1 θ}, . . . , {pn θ} Pn {qn θ} |=tot {pθ} S {qθ},where θ ≡ [z := m].⊓⊔Proof. See Exercise 4.7.Finally, we shall need the following observation.Lemma 4.2.
(Fresh Variable) Suppose that z is an integer variable thatdoes not appear in D, S or q. Then|=tot {∃z ≥ 0 : p} S {q} iff for all m ≥ 0, |=tot {p[z := m]} S {q}.⊓⊔Proof. See Exercise 4.8.Theorem 4.5. (Soundness of the Recursion II Rule)Assume that D = P1 :: S1 , . . . , Pn :: Sn . Suppose that{p1 } P1 {q1 }, . . . , {pn } Pn {qn } ⊢ {p} S {q}and for i = 1, . . . , n{p1 ∧ t < z} P1 {q1 }, . . .
, {pn ∧ t < z} Pn {qn } ⊢ {pi ∧ t = z} Si {qi }andpi → t ≥ 0,where the fresh integer variable z is treated in the proofs as a constant. Then|=tot {p} S {q}.Proof. By the Soundness Theorem 4.3 we have{p1 } P1 {q1 }, . . . , {pn } Pn {qn } |=tot {p} S {q}.(4.7)Further, by the Instantiation Theorem 4.4, we deduce for i = 1, .
. . , n from{p1 ∧ t < z} P1 {q1 }, . . . , {pn ∧ t < z} Pn {qn } ⊢ {pi ∧ t = z} Si {qi }that for all m ≥ 04.3 Verification143{p1 ∧ t < m} P1 {q1 }, . . . , {pn ∧ t < m} Pn {qn } ⊢ {pi ∧ t = m} Si {qi }.Hence by the Soundness Theorem 4.3, for i = 1, . . . , n and m ≥ 0{p1 ∧ t < m} P1 {q1 }, . . .
, {pn ∧ t < m} Pn {qn } |=tot {pi ∧ t = m} Si {qi }.(4.8)We now show|=tot {pi } Pi {qi }(4.9)for i = 1, . . . , n.To this end, we exploit the fact that the integer variable z appears neitherin pi nor in t. Therefore the assertions pi and ∃z : (pi ∧ t < z) are equivalent.Moreover, since pi → t ≥ 0, we have∃z : (pi ∧ t < z) → ∃z ≥ 0 : (pi ∧ t < z).So it suffices to show|=tot {∃z ≥ 0 : (pi ∧ t < z)} Pi {qi }for i = 1, . . .
, n. Now, by the Fresh Variable Lemma 4.2 it suffices to provethat for all m ≥ 0|=tot {pi ∧ t < m} Pi {qi }.for i = 1, . . . , n. We proceed by induction on m.Induction basis: m = 0. By assumption, pi → t ≥ 0 holds for i = 1, . . . , n, so(pi ∧ t < 0) → false. Hence the claim holds as |=tot {false} Pi {qi }.Induction step: m → m + 1. By the induction hypothesis, we have|=tot {pi ∧ t < m} Pi {qi },for i = 1, . . . , n.By (4.8), we obtain |=tot {pi ∧ t = m} Si {qi } for i = 1, .
. . , n, so bythe Input/Output Lemma 4.1(ii) we have |=tot {pi ∧ t = m} Pi {qi } fori = 1, . . . , n. But t < m + 1 is equivalent to t < m ∨ t = m, so we obtain |=tot {pi ∧ t < m + 1} Pi {qi }, for i = 1, . . . , n.This proves (4.9) for i|=tot {p} S {q}.=1, . . . , n. Now (4.7) and (4.9) imply⊓⊔With this theorem we can state the following soundness result.Corollary 4.2. (Soundness of TR) The proof system TR is sound for totalcorrectness of recursive programs.1444 Recursive ProgramsProof. The proof combines Theorem 4.5 with Theorem 3.1(ii) on soundnessof the proof system TW and Theorem 3.7(iii) on soundness of the auxiliaryrules.⊓⊔4.4 Case Study: Binary SearchConsider a section a[f irst : last] (so f irst ≤ last) of an integer array a that issorted in increasing order.
Given a variable val, we want to find out whetherits value occurs in the section a[f irst : last], and if yes, to produce the indexmid such that a[mid] = val. Since a[f irst : last] is sorted, this can be doneby means of the recursive binary search procedure shown in Figure 4.3. (Aniterative version of this program is introduced in Exercise 4.10.)BinSearch :: mid := (f irst + last) div 2;if f irst 6= lastthen if a[mid] < valthen f irst := mid + 1; BinSearchelse if a[mid] > valthen last := mid; BinSearchfififiFig. 4.3 The program BinSearch.We now prove correctness of this procedure.
To refer in the postconditionto the initial values of the variables f irst and last, we introduce variables fand l. Further, to specify that the array section a[f irst : last] is sorted, weuse the assertion sorted(a[f irst : last]) defined bysorted(a[f irst : last]) ≡ ∀x, y : (f irst ≤ x ≤ y ≤ last → a[x] ≤ a[y]).Correctness of the BinSearch procedure is then expressed by the correctness formula{p}BinSearch{q},wherep ≡ f = f irst ∧ l = last ∧ f irst ≤ last ∧ sorted(a[f irst : last]),q ≡ f ≤ mid ≤ l ∧ (a[mid] = val ↔ ∃x ∈ [f : l] : a[x] = val).4.4 Case Study: Binary Search145The postcondition q thus states that mid is an index in the section a[f : l]and a[mid] = val exactly when the value of the variable val appears in thesection a[f : l].Partial CorrectnessIn order to prove the partial correctness it suffices to show{p}BinSearch{q} ⊢ {p}S{q},where ⊢ refers to a sound proof system for partial correctness and S denotesthe body of BinSearch, and apply the simplified form of the recursion ruleof Section 4.3.To deal with the recursive calls of BinSearch we adapt the assumption{p} BinSearch {q} using the substitution rule and the invariance rule introduced in Section 3.8, to derive the correctness formulas{p[f := (f + l) div 2 + 1] ∧ r1 } BinSearch {q[f := (f + l) div 2 + 1] ∧ r1 }and{p[l := (f + l) div 2] ∧ r2 } BinSearch {q[l := (f + l) div 2] ∧ r2 },wherer1 ≡ sorted(a[f : l]) ∧ a[(f + l) div 2] < val,r2 ≡ sorted(a[f : l]) ∧ val < a[(f + l) div 2].Then, as in the case of the factorial program, we present the proof fromthese two assumptions in the form of a proof outline that we give in Figure 4.4.Since we use the if B then S fi statement twice in the procedure body, weneed to justify the appropriate two applications of the rule for this statement,introduced in Exercise 3.11.
To this end, we need to check the following twoimplications:(p ∧ mid = (f irst + last) div 2 ∧ f irst = last) → qand(p ∧ mid = (f irst + last) div 2 ∧ f irst 6= last ∧ a[mid] = val) → q,that correspond to the implicit else branches. The first implication holds,since(p ∧ mid = (f irst + last) div 2 ∧ f irst = last)→ mid = f = l→ a[mid] = val ↔ ∃x ∈ [f : l] : a[x] = val,1464 Recursive Programs{p}mid := (f irst + last) div 2;{p ∧ mid = (f irst + last) div 2}if f irst 6= lastthen{p ∧ mid = (f irst + last) div 2 ∧ f irst 6= last}if a[mid] < valthen{p ∧ mid = (f irst + last) div 2 ∧ f irst 6= last ∧ a[mid] < val}{(p[f := (f + l) div 2 + 1] ∧ r1 )[f irst := mid + 1]}f irst := mid + 1;{p[f := (f + l) div 2 + 1] ∧ r1 }BinSearch{q[f := (f + l) div 2 + 1] ∧ r1 }{q}else{p ∧ mid = (f irst + last) div 2 ∧ f irst 6= last ∧ a[mid] ≥ val}if a[mid] > valthen{p ∧ mid = (f irst + last) div 2 ∧ f irst 6= last ∧ a[mid] > val}{(p[l := (f + l) div 2] ∧ r2 )[last := mid]}last := mid;{p[l := (f + l) div 2] ∧ r2 }BinSearch{q[l := (f + l) div 2] ∧ r2 }{q}fi{q}fi{q}fi{q}Fig.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
