3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 32

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 32)

Then|= {p} begin local x̄ := t̄; S end {q}.Proof. Suppose that σ |= p and τ ∈ M[[begin local x̄ := t̄; S end]](σ).Then by the Block Lemma 5.4 for some sequence of values d¯¯ ∈ M[[x̄ := t̄; S]](σ).τ [x̄ := d]¯ |= q. But {x̄} ∩ f ree(q) = ∅, hence τ |= q. ⊓So by the assumption τ [x̄ := d]⊔To deal with the instantiation rule we shall need the following observationanalogous to the Change and Access Lemma 3.4.Lemma 5.5. (Change and Access) Assume thatD = P1 (ū1 ) :: S1 , . .

. , Pn (ūn ) :: Sn .For all proper states σ and τ , i = 1, . . . , n and sequences of expressions t̄such that var(t̄) ∩ change(D) = ∅,5.3 Verification169τ ∈ M[[Pi (t̄)]](σ)impliesτ [x̄ := σ(t̄)] ∈ M[[Pi (x̄)]](σ[x̄ := σ(t̄)]),whenever var(x̄) ∩ var(D) = ∅.⊓⊔Proof. See Exercise 5.4.Theorem 5.2. (Soundness of the Instantiation Rule)Assume that D = P1 (ū1 ) :: S1 , . . .

, Pn (ūn ) :: Sn and suppose that|= {p} Pi (x̄) {q},where var(x̄) ∩ var(D) = ∅. Then|= {p[x̄ := t̄]} Pi (t̄) {q[x̄ := t̄]}for all sequences of expressions t̄ such that var(t̄) ∩ change(D) = ∅.Proof. Suppose that σ |= p[x̄ := t̄] and τ ∈ M[[Pi (t̄)]](σ). By the Simultaneous Substitution Lemma 2.5, σ[x̄ := σ(t̄)] |= p, and by the Change andAccess Lemma 5.5,τ [x̄ := σ(t̄)] ∈ M[[Pi (x̄)]](σ[x̄ := σ(t̄)]).Hence by the assumption about the generic procedure call Pi (x̄) we haveτ [x̄ := σ(t̄)] |= q, so, again by the Simultaneous Substitution Lemma 2.5,τ |= q[x̄ := t̄].⊓⊔Finally, we deal with the recursion III rule. Recall that the provabilitysign ⊢ refers to the proof system PW augmented with the (modified as explained earlier in this section) auxiliary axioms and rules and the block andinstantiation rules, in the implicit context of the set of procedure declarationsD.We shall need a counterpart of the Soundness Lemma 4.1, in which we usethis implicit context D, as well.

We write here{p1 } P1 (t̄1 ) {q1 }, . . . , {pn } Pn (t̄n ) {qn } |= {p} S {q}when the following holds:for all sets of procedure declarations D′ such that var(D′ ) ⊆ var(D)if |= {pi } D′ | Pi (t̄i ) {qi }, for i ∈ {1, . . . , n}, then |= {p} D′ | S {q},where, as in the Input/Output Lemma 5.1, D′ | S means that we evaluate Sin the context of the set D′ of the procedure declarations.1705 Recursive Programs with ParametersTheorem 5.3. (Soundness of Proof from Assumptions)We have that{p1 } P1 (t̄1 ) {q1 }, . .

. , {pn } Pn (t̄n ) {qn } ⊢ {p} S {q}implies{p1 } P1 (t̄1 ) {q1 }, . . . , {pn } Pn (t̄n ) {qn } |= {p} S {q}.⊓⊔Proof. See Exercise 5.5.Theorem 5.4. (Soundness of the Recursion III Rule)Assume that Pi (ūi ) :: Si ∈ D for i ∈ {1, . . . , n}. Suppose that{p1 } P1 (t̄1 ) {q1 }, . . . , {pn } Pn (t̄1 ) {qn } ⊢ {p} S {q},and for i ∈ {1, . . . , n}{p1 } P1 (t̄1 ) {q1 }, . .

. , {pn } Pn (t̄n ) {qn } ⊢{pi } begin local ūi := t̄i ; Si end {qi }.Then|= {p} S {q}.Proof. We proceed as in the proof of the Soundness Theorem 4.2. By theSoundness Theorem 5.3{p1 } P1 (t̄1 ) {q1 }, . . . , {pn } Pn (t̄n ) {qn } |= {p} S {q}(5.7)and for i ∈ {1, .

. . , n}{p1 } P1 (t̄1 ) {q1 }, . . . , {pn } Pn (t̄n ) {qn }|= {pi } begin local ūi := t̄i ; Si end {qi }.(5.8)|= {pi } Pi (t̄i ) {qi }(5.9)We first showfor i ∈ {1, . . . , n}.In the proof write D′ | S when we mean S in the context of the set D′ ofprocedure declarations. By the Input/Output Lemma 5.1(i) and (iii) we havesoM[[D | Pi (t̄i )]]S∞= k=0 M[[Pi (t̄i )k ]]S∞= M[[Pi (t̄i )0 ]] ∪ k=0 M[[Dk | Pi (t̄i )]]S∞= k=0 M[[Dk | Pi (t̄i )]],5.3 Verification171|= {pi } D | Pi (t̄i ) {qi } iff for all k ≥ 0 we have |= {pi } Dk | Pi (t̄i ) {qi }.We now prove by induction on k that for all k ≥ 0|= {pi } Dk | Pi (t̄i ) {qi },for i ∈ {1, . .

. , n}.Induction basis. Since Si0 = Ω, by definition |= {pi } D0 | Pi (t̄i ) {qi }, fori ∈ {1, . . . , n}.Induction step. By the induction hypothesis we have|= {pi } Dk | Pi (t̄i ) {qi },for i ∈ {1, . . . , n}. Fix i ∈ {1, . . ., n}. Since var(Dk ) ⊆ var(D), by (5.8) weobtain|= {pi } Dk | begin local ūi := t̄i ; Si end {qi }.Next, by the Input/Output Lemma 5.1(i) and (ii)M[[Dk | begin local ūi := t̄i ; Si end]]= M[[(begin local ūi := t̄i ; Si end)k+1 ]]= M[[Dk+1 | (begin local ūi := t̄i ; Si end)k+1 ]]= M[[Dk+1 | Pi (t̄i )]],hence |= {pi } Dk+1 | Pi (t̄i ) {qi }.This proves (5.9) for i ∈ {1, .

. . , n}. Now (5.7) and (5.9) 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 5.1. (Soundness of PRP) The proof system PRP is sound forpartial correctness of recursive programs with parameters.Proof. The proof combines Theorems 5.1, 5.2 and 5.4 with Theorem 3.1(i)on soundness of the proof system PW and Theorem 3.7(i),(ii) on soundnessof the auxiliary rules.⊓⊔Next, we establish soundness of the proof system TRP for total correctnessof recursive programs with parameters.

We proceed in an analogous way asin the case of the parameterless procedures.Theorem 5.5. (Soundness of TRP) The proof system TRP is sound fortotal correctness of recursive programs with parameters.1725 Recursive Programs with ParametersProof. See Exercise 5.7.⊓⊔5.4 Case Study: QuicksortIn this section we establish correctness of the classical Quicksort sorting procedure, originally introduced in Hoare[1962].

For a given array a of typeinteger → integer and integers x and y this algorithm sorts the sectiona[x : y] consisting of all elements a[i] with x ≤ i ≤ y. Sorting is accomplished‘in situ’, i.e., the elements of the initial (unsorted) array section are permutedto achieve the sorting property.

We consider here the following version ofQuicksort close to the one studied in Foley and Hoare [1971]. It consists of arecursive procedure Quicksort(m, n), where the formal parameters m, n andthe local variables v, w are all of type integer:Quicksort(m, n) ::if m < nthen P artition(m, n);beginlocal v, w := ri, le;Quicksort(m, v);Quicksort(w, n)endfiQuicksort calls a non-recursive procedure P artition(m, n) which partitionsthe array a suitably, using global variables ri, le, pi of type integer standingfor pivot, left, and right elements:P artition(m, n) ::pi := a[m];le, ri := m, n;while le ≤ ri dowhile a[le] < pi do le := le + 1 od;while pi < a[ri] do ri := ri − 1 od;if le ≤ ri thenswap(a[le], a[ri]);le, ri := le + 1, ri − 1fiodHere, as in Section 3.9, for two given simple or subscripted variables u and vthe program swap(u, v) is used to swap the values of u and v.

So we stipulatethat the following correctness formula{x = u ∧ y = v} swap(u, v) {x = v ∧ y = u}5.4 Case Study: Quicksort173holds in the sense of partial and total correctness, where x and y are freshvariables.In the following D denotes the set of the above two procedure declarationsand SQ the body of the procedure Quicksort(m, n).Formal Problem SpecificationCorrectness of Quicksort amounts to proving that upon termination of theprocedure call Quicksort(m, n) the array section a[m : n] is sorted and is apermutation of the input section.

To write the desired correctness formulawe introduce some notation. First, recall from Section 4.5 the assertionsorted(a[f irst : last]) ≡ ∀x, y : (f irst ≤ x ≤ y ≤ last → a[x] ≤ a[y])stating that the integer array section a[f irst : last] is sorted. To express thepermutation property we use an auxiliary array a0 in the section a0 [x : y]of which we record the initial values of a[x : y].

Recall from Section 3.9 theabbreviationsbij(β, x, y) ≡ β is a bijection on N ∧ ∀ i 6∈ [x : y] : β(i) = istating that β is a bijection on N which is the identity outside the interval[x : y] andperm(a, a0 , [x : y]) ≡ ∃ β : (bij(β, x, y) ∧ ∀i : a[i] = a0 [β(i)])specifying that the array section a[x : y] is a permutation of the array sectiona0 [x : y] and that a and a0 are the same elsewhere.We can now express the correctness of Quicksort by means of the followingcorrectness formula:Q1{a = a0 } Quicksort(x, y) {perm(a, a0 , [x : y]) ∧ sorted(a[x : y])}.To prove correctness of Quicksort in the sense of partial correctness we proceed in stages and follow the modular approach explained in Section 5.3.In other words, we establish some auxiliary correctness formulas first, usingamong others the recursion III rule.

Then we use them as premises in orderto derive other correctness formulas, also using the recursion III rule.Properties of P artitionIn the proofs we shall use a number of properties of the P artition procedure.This procedure is non-recursive, so to verify them it suffices to prove the1745 Recursive Programs with Parameterscorresponding properties of the procedure body using the proof systems PWand TW.More precisely, we assume the following properties of P artition in thesense of partial correctness:P1{true} P artition(m, n) {ri ≤ n ∧ m ≤ le},P2{x′ ≤ m ∧ n ≤ y ′ ∧ perm(a, a0 , [x′ : y ′ ])}P artition(m, n){x′ ≤ m ∧ n ≤ y ′ ∧ perm(a, a0 , [x′ : y ′ ])},P3{true}P artition(m, n){ le > ri ∧( ∀ i ∈ [m : ri] : a[i] ≤ pi) ∧( ∀ i ∈ [ri + 1 : le − 1] : a[i] = pi) ∧( ∀ i ∈ [le : n] : pi ≤ a[i])},and the following property in the sense of total correctness:PT4 {m < n} P artition(m, n) {m < le ∧ ri < n}.Property P1 states the bounds for ri and le.

Характеристики

Список файлов книги