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

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

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

Then the array section a[k − 1 : n] with a[k − 1] = y ensures thetruth of the second conjunct of q[y := next]. Indeed, we then have a[k − 1] 6=null∧a[k−1].val 6= 0∧a[k−1].next = a[k], as by the definition of the meaningof an assertion both this 6= null and val = this.val ∧ next = this.next.We now obtain the desired conclusion by an application of the consequencerule.⊓⊔Claim 3.

{this = y ∧ val 6= 0 ∧ next = null} return := null {q}.Proof. We show(this = y ∧ val 6= 0 ∧ next = null) → q[return := null],from which the claim follows by the assignment axiom and the consequencerule.The first conjunct of q[return := null] holds since it contains null = nullas a disjunct. Next, to satisfy the second conjunct of q[return := null] underthe assumption this = y ∧ val 6= 0 ∧ next = null, it suffices to take array asuch that a[k] = y and n = k + 1. Indeed, we then have both y = a[k] anda[n] = null. Moreover, the third conjunct of p[return := this] holds sincewe then have a[k] 6= null ∧ a[k].val 6= 0 ∧ a[k].next = a[k + 1], as by thedefinition of the meaning of an assertion this 6= null.⊓⊔Total CorrectnessIn order for this.f ind to terminate we require that the chain of objectsstarting from this and linked by next ends with null or contains an objectthat stores zero.To express this we first introduce the following assertion p:p ≡ k ≤ n ∧ (a[n] = null ∨ a[n].val = 0)∧∀ i ∈ [k : n − 1] : (a[i] 6= null ∧ a[i].next = a[i + 1]),which states that the section a[k : n] stores a linked list of objects that endswith null or with an object that stores zero.

Let r be defined byr ≡ y = a[k] ∧ y 6= null ∧ p.We now prove{∃ a : ∃ k : ∃ n ≥ k : r[y := this]} this.f ind {true}2306 Object-Oriented Programsin the sense of total correctness.As the bound function we chooset ≡ n − k.As in the proof of partial correctness we use the normal object variable y asa generic representation of the caller of the method f ind.We now show{r ∧ t < z} y.f ind {true} ⊢{r ∧ t = z} begin local this := y; S end {true}(6.4)where, as above, S denotes the body of the method f ind and where ⊢ refersto the proof system TOP with the recursion VIII rule omitted.To this end, we again present the proof in the form of a proof outline thatwe give in Figure 6.5.We only need to justify the correctness formula involving the method callnext.f ind. To this end, we first apply the instantiation II rule to the assumption and replace y by next:{r[y := next] ∧ n − k < z} next.f ind {true}.Next, we apply the substitution rule and replace k by k + 1:{r[k, y := k + 1, next] ∧ n − (k + 1) < z} next.f ind {true}.Now note that(r ∧ this = y ∧ t = z ∧ val 6= 0 ∧ next 6= null)→ (r[k, y := k + 1, next] ∧ n − (k + 1) < z).Indeed, we have by the definition of rr ∧ this = y ∧ val 6= 0→ (a[n] = null ∨ a[n].val = 0) ∧ this = a[k] ∧ val 6= 0 ∧ k ≤ n→ (a[n] = null ∨ a[n].val = 0) ∧ a[k] 6= null ∧ a[k].val 6= 0 ∧ k ≤ n→ k < n,where the second implication holds sincethis 6= null ∧ val = this.val.Hence6.8 Case Study: Zero Search in Linked List231{r ∧ t = z}begin local{r ∧ t = z}this := y;{r ∧ this = y ∧ t = z}if val = 0then{true}return := this{true}else{r ∧ this = y ∧ t = z ∧ val 6= 0}if next 6= nullthen{r ∧ this = y ∧ t = z ∧ val 6= 0 ∧ next 6= null}{r[k, y := k + 1, next] ∧ n − (k + 1) < z}next.f ind{true}else{true}return := null{true}fi{true}fi{true}end{true}Fig.

6.5 Proof outline showing termination of the f ind method.→→→→(r ∧ this = y ∧ t = z ∧ val 6= 0 ∧ next 6= null)(this = a[k] ∧ k < n ∧ next 6= null ∧ p)(this = a[k] ∧ a[k].next = a[k + 1] ∧ next 6= null ∧ p[k := k + 1])(next = a[k + 1] ∧ next 6= null ∧ p[k := k + 1])r[k, y := k + 1, next],where we make use of the fact that next = this.next.Moreovert = z → n − (k + 1) < z.This completes the justification of the proof outline. By the recursion VI rulewe now derive from (6.4) and the fact that r → y 6= null the correctnessformula2326 Object-Oriented Programs{r} y.f ind {true}.By the instantiation II rule we now obtain{r[y := this]} this.f ind {true},from which the desired correctness formula follows by the elimination rule.6.9 Case Study: Insertion into a Linked ListWe now return to the insert method defined in Example 6.21:insert :: begin localz := next;next := new;next.setnext(z)endwhere the method setnext is defined bysetnext(u) :: next := u.In order to express the correctness of the insert method we introduce as inthe previous case study an array variable a ∈ V ar of type integer → objectto store the list of objects linked by their instance variable next.

Further,we introduce the simple object variable y ∈ V ar to represent a generic callerand the integer variable k ∈ V ar to denote the position of the insertion.As a precondition we use the assertionp ≡ y = a[k] ∧ k ≥ 0 ∧ ∀n ≥ 0 : a[n].next = a[n + 1],which states that y appears at the kth position and that the objects storedin a are linked by the value of their instance variable next. Note that we alsorequire for a[n] = null that a[n].next = a[n+1]. By putting null.next = nullthis requirement can easily be met.Insertion of a new object at position k is described by the postconditionq ≡ q0 ∧ q1 ∧ q2 ,where• q0 ≡ ∀n ≥ 0 : if a[n] 6= a[k] then a[n].next = a[n + 1] fi,• q1 ≡ ∀n ≥ 0 : a[n] 6= a[k].next,• q2 ≡ a[k].next.next = a[k + 1].The assertion q0 states that the chain of objects is ‘broken’ at the kth position. The assertion q1 states that the instance variable next of the object6.9 Case Study: Insertion into a Linked List233at position k points to a new object.

Finally, the assertion q2 states that theinstance variable next of this new object refers to the object at position k +1.We prove{p} y.insert {q}in the sense of partial correctness. By the simplified version of the recursion Vrule, it suffices to prove{p} begin local this := y; S end {q},where S denotes the body of the method insert.

For this it suffices, by therecursion VII rule, to prove for suitable assertions p′ and q ′{p′ } next.setnext(z) {q ′ } ⊢ {p} begin local this := y; S end {q}(6.5)and{p′ } begin local this, u := next, z; next := u end {q ′ },(6.6)where ⊢ refers to the proof system POC with the recursion VII rule omitted.We prove (6.5) and (6.6) in the form of proof outlines given below inFigures 6.6 and 6.7, respectively.In these proofs we usep′ ≡ q0 ∧ q1 ∧ k ≥ 0 ∧ this = a[k] ∧ z = a[k + 1]andq ′ ≡ q.For the justification of these proof outlines we introduce the abbreviationt(l, v) defined byt(l, v) ≡ (a[l].next)[next := v]≡ if a[l] = this then v else a[l].next fi,where l ∈ V ar ranges over simple integer variables and v ∈ V ar ranges oversimple object variables.To justify the proof outline in Figure 6.6 it suffices to establish the followingfour claims.Claim 1.

{p} this := y {p ∧ this = y}.Proof. By the assignment axiom for normal variables we have{p ∧ y = y} this := y {p ∧ this = y}.So we obtain the desired result by a trivial application of the consequencerule.⊓⊔Claim 2. {p ∧ this = y} z := next {p ∧ this = y ∧ z = next}.2346 Object-Oriented Programs{p}begin local{p}this := y;{p ∧ this = y}begin local{p ∧ this = y}z := next;{p ∧ this = y ∧ z = next}{p ∧ k ≥ 0 ∧ this = a[k] ∧ z = a[k + 1]}next := new;{q0 ∧ q1 ∧ k ≥ 0 ∧ this = a[k] ∧ z = a[k + 1]}next.setnext(z){q}end{q}end{q}Fig.

6.6 Proof outline showing partial correctness of the insert method.Proof. This claim also follows by an application of the assignment axiomfor normal variables and a trivial application of the consequence rule.⊓⊔Claim 3. (p ∧ this = y ∧ z = next) → (k ≥ 0 ∧ this = a[k] ∧ z = a[k + 1]).Proof. It suffices to observe that• (p ∧ this = y) → this = a[k],• (this = a[k] ∧ z = next) → z = a[k].next,• p → a[k].next = a[k + 1].For the second implication recall that z = next stands for z = this.next.⊓⊔Claim 4. {p ∧ k ≥ 0 ∧ this = a[k] ∧ z = a[k + 1]}next := new{q0 ∧ q1 ∧ k ≥ 0 ∧ this = a[k] ∧ z = a[k + 1]}.Proof. First, we introduce a fresh simple object variable x ∈ V ar andcalculateq0 [next := x] ≡ ∀n ≥ 0 : if a[n] 6= a[k] then t(n, x) = a[n + 1] fi,where t(n, x) ≡ if a[n] = this then x else a[n].next fi.

We observe thatthis = a[k] ∧ a[n] 6= a[k] implies a[n] 6= this and that a[n] 6= this implies t(n, x) = a[n].next. Replacing t(n, x) in q0 [next := x] by a[n].next we6.9 Case Study: Insertion into a Linked List235obtain q0 itself. So we have thatthis = a[k] ∧ q0 → q0 [next := x].Since x does not occur in this = a[k] ∧ q0 , we havethis = a[k] ∧ q0 ≡ (this = a[k] ∧ q0 )[x := new]and derive by the object creation rule{this = a[k] ∧ q0 } next := new {q0 }.Since p → q0 , we derive by the consequence rule that{p ∧ this = a[k]} next := new {q0 }.(6.7)Next, we calculateq1 [next := x] ≡ ∀n ≥ 0 : a[n] 6= t(k, x),where t(k, x) ≡ if a[k] = this then x else a[k].next fi.

Sincea[n] 6= t(k, x) ↔ if a[k] = this then a[n] 6= x else a[n] 6= a[k].next fiit follows that∀n ≥ 0 : if a[k] = this then a[n] 6= x else a[n] 6= a[k].next fi→ q1 [next := x].Now we calculateif a[k] = this then a[n] 6= x else a[n] 6= a[k].next fi[x := new]≡ if (a[k] = this)[x := new]then (a[n] 6= x)[x := new]else (a[n] 6= a[k].next)[x := new]fi≡ if a[k] = this then ¬false else a[n] 6= a[k].next fi.So(∀n ≥ 0 : if a[k] = this then a[n] 6= x else a[n] 6= a[k].next fi)[x := new]≡ ∀n ≥ 0 : if a[k] = this then ¬false else a[n] 6= a[k].next fi.Further, we havethis = a[k] → ∀n ≥ 0 : if a[k] = this then ¬false else a[n] 6= a[k].next fi.So by the object creation rule and the consequence rule, we derive2366 Object-Oriented Programs{this = a[k]} next := new {q1 }.(6.8)By an application of the conjunction rule to the correctness formulas (6.7)and (6.8), we therefore obtain{p ∧ this = a[k]} next := new {q0 ∧ q1 }.An application of the invariance rule then gives us the desired result.⊓⊔{q0 ∧ q1 ∧ k ≥ 0 ∧ this = a[k] ∧ z = a[k + 1]}begin local{q0 ∧ q1 ∧ k ≥ 0 ∧ this = a[k] ∧ z = a[k + 1]}this, u := next, z;{q0 ∧ q1 ∧ k ≥ 0 ∧ this = a[k].next ∧ u = a[k + 1]}next := u{q}end{q}Fig.

6.7 Proof outline showing partial correctness of the setnext method.To justify the proof outline in Figure 6.7 it suffices to establish the followingtwo claims.Claim 5. {q0 ∧ q1 ∧ k ≥ 0 ∧ this = a[k] ∧ z = a[k + 1]}this, u := next, z{q0 ∧ q1 ∧ k ≥ 0 ∧ this = a[k].next ∧ u = a[k + 1]}.Proof. By the assignment axiom for normal variables and the consequencerule, it suffices to observe that this = a[k] → next = a[k].next.⊓⊔Claim 6. {q0 ∧ q1 ∧ k ≥ 0 ∧ this = a[k].next ∧ u = a[k + 1]}next := u{q}.Proof.

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

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