3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 41
Текст из файла (страница 41)
On the otherhand, in pure global expressions we can dereference object expressions, likein s.x where s is an object expression.An assertion is called pure if it is built up from pure global expressionsby Boolean connectives and quantification, but not over object variables orarray variables with value type object. Such quantification requires a moresophisticated analysis as the following example shows.6.7 Object Creation221Example 6.25.
Consider the assertionp ≡ ∀x : ∃n : a[n] = x,where a is a normal array variable of type integer → object, n ∈ V ar is aninteger variable, and x ∈ V ar is a simple object variable. Note that p is notpure. Since we restrict the semantics of assertions to consistent states, theuniversal quantifier ∀x and the elements of the array a range over createdobjects. Thus p states that the array a stores all created objects (and onlythose). As a consequence p is affected by an object creation statement u :=new.
More specifically, we do not have{p} u := new {p},so the invariance axiom does not hold any more. In fact,{p} u := new {∀n : a[n] 6= u}⊓⊔holds.First, we define the substitution operation for expressions. The formaldefinition of s[x := new], where s 6≡ x is a pure global expression and x ∈ V aris a simple object variable, proceeds by induction on the structure of s. Wehave the following main cases:• if s ≡ x.u and the (possibly subscripted) instance variable u is of type Tthens[x := new] ≡ init T ,• if s ≡ s1 .u for s1 6≡ x thens[x := new] ≡ s1 [x := new].u[x := new],• if s ≡ (s1 = s2 ) for s1 6≡ x and s2 6≡ x thens[x := new] ≡ (s1 [x := new] = s2 [x := new]),• if s ≡ (x = t) (or s ≡ (t = x)) for t 6≡ x thens[x := new] ≡ false,• if s ≡ (x = x) thens[x := new] ≡ true.The other cases are standard.Example 6.26. Let s ≡ if B then s1 else s2 fi be a pure global expressionand x ∈ V ar be a simple object variable.
Then2226 Object-Oriented Programss[x := new] ≡ if B[x := new] then s1 [x := new] else s2 [x := new] fi.Note that this is well-defined: since s cannot be an object expression wehave that s1 6≡ x and s2 6≡ x. Similarly, if s ≡ a[s1 , . . . , sn ] is a pure globalexpression thens[x := new] ≡ a[s1 [x := new], . . . , sn [x := new]].Note that si 6≡ x because si cannot be an object expression, for i ∈ {1, . . . , n}.Next we calculate(x = this)[x := new] ≡ false ,(a[s] = x)[x := new] ≡ false ,and(x.y = this)[x := new]≡ (x.y)[x := new] = this[x := new]≡ initT = this,where the instance variable y is of type T .⊓⊔To prove correctness of the substitution operation [x := new] for objectcreation we need the following lemma which states that no pure global expression other than x can refer to the newly created object.Lemma 6.10.
Let s 6≡ x be a pure global object expression and x ∈ V ar bea simple object variable. Further, let σ be a consistent proper state. Thenσ[x := new](s) 6= σ[x := new](x).Proof. The proof proceeds by induction on the structure of s (see Exercise 6.18).⊓⊔The following example shows that in the above lemma the restriction topure global expressions and to consistent (proper) states is necessary.Example 6.27. Let x be a normal object variable. Then we have for globalexpressions s of the form• s ≡ id(x), where the constant id is interpreted as the identity function onobjects, and• s ≡ if true then x else y fi, where y is also a normal object variable,that σ[x := new](s) = σ[x := new](x).Next, consider a normal object variable y 6≡ x and a state σ such thatσ(y) = ν(σ). Then σ(σ(y))(created ) = false by the definition of the function ν. So σ is not a consistent state.
We calculate that σ[x := new](y) =σ(y) = σ[x := new](x).⊓⊔6.7 Object Creation223We extend the substitution operation to pure assertions along the lines ofSection 2.7. We have the following substitution lemma.Lemma 6.11. (Substitution for Object Creation) For all pure globalexpressions s, all pure assertions p, all simple object variables x and all consistent proper states σ,(i) σ(s[x := new]) = σ[x := new](s),(ii) σ |= p[x := new] iff σ[x := new] |= p.Proof. The proof proceeds by induction on the complexity of s and p, usingLemma 6.10 for the base case of Boolean expressions (see Exercise 6.19).
⊓⊔The following lemma shows that the restriction concerning conditionalexpressions in pure assertions does not affect the expressiveness of the assertion language because conditional expressions can always be removed. Therestriction only simplified the definition of substitution operator [x := new].Lemma 6.12. (Conditional Expressions) For every assertion p there exists a logically equivalent assertion which does not contain conditional expressions.Proof. See Exercise 6.20.⊓⊔The following example gives an idea of the proof.Example 6.28. A Boolean conditional expression if B then s else t fi canbe eliminated using the following logical equivalence:if B then s else t fi ↔ (B ∧ s) ∨ (¬B ∧ t).A conditional expression if B then s else t fi in the context of an equalityor a dereferencing operator can be moved outside as follows:• (if B then s else t fi = t′ ) = if B then s = t′ else t = t′ fi,• if B then s else t fi.y = if B then s.y else t.y fi.In general, we have the equalityop(t1 , .
. . , if B then s else t fi, . . . , tn )= if B then op(t1 , . . . , s, . . . , tn ) else op(t1 , . . . , t, . . . , tn ) fifor every constant op of a higher type.⊓⊔VerificationThe correctness notions for object-oriented programs with object creation aredefined in the familiar way using the semantics M and Mtot (note that the2246 Object-Oriented Programspartial correctness and the total correctness semantics of an object creationstatement coincide). To ensure that when studying program correctness welimit ourselves to meaningful computations of object-oriented programs, weprovide the following new definition of the meaning of an assertion:[[p]] = { σ | σ is a consistent proper state such thatσ(this) 6= null and σ |= p },and say that an assertion p is is true, or holds, if[[p]] = {σ | σ is a consistent proper state such that σ(this) 6= null}.We have the following axiom and rule for object creation.AXIOM 21: OBJECT CREATION{p[x := new]} x := new {p},where x ∈ V ar is a simple object variable and p is a pure assertion.RULE 22: OBJECT CREATIONp′ → p[u := x]{p [x := new]} u := new {p}′where u is a subscripted normal object variable or a (possibly subscripted)instance object variable, x ∈ V ar is a fresh simple object variable which doesnot occur in p, and p′ is a pure assertion.The substitution [u := x] replaces every possible alias of u by x.
Note thatthis rule models the object creation u := new by the statementx := new; u := x,and as such allows for the application of the substitution [x := new] definedabove.Example 6.29. Consider the object creation statementnext := newfor the object instance variable next and the postconditionp ≡ y.next = next.We wish to prove{y = this} next := new {p}.First, we calculate for a fresh variable x ∈ V ar:6.7 Object Creation225p[next := x] ≡ if y = this then x else y.next fi = x.Consider nowp′ ≡ if y = this then x = x else y.next = x fi.Observe that p′ → p[next := x]. Next, we calculatep′ [x := new]≡ if (y = this)[x := new]then(x = x)[x := new] else (y.next = x)[x := new] fi≡ if y = this then true else false fi,which is logically equivalent to y = this. By the object creation rule and theconsequence rule, we thus derive{y = this} next := new {p},⊓⊔as desired.To prove partial correctness of object-oriented programs with objectcreation we use the following proof system POC :PROOF SYSTEM POC :This system consists of the group of axiomsand rules 1–6, 10, 14, 18, 19, 21, 22 and A2–A7.Thus POC is obtained by extending the proof system POP by the axiom andrule for object creation.To prove total correctness of object-oriented programs with object creationwe use the following proof system TOC :PROOF SYSTEM TOC :This system consists of the group of axiomsand rules 1–4, 6, 7, 10, 14, 18, 20–22 and A3–A7.Thus TOC is obtained by extending the proof system TOP by the axiom andrule for object creation.SoundnessWe have the following soundness theorem for object creation.2266 Object-Oriented ProgramsTheorem 6.3.
(Soundness of POC and TOC)(i) The proof system POC is sound for partial correctness of object-orientedprograms with object creation.(ii) The proof system TOC is sound for total correctness of object-orientedprograms with object creation.Proof. Axiom 21 is true and rule 22 is sound, see Exercise 6.21.⊓⊔6.8 Case Study: Zero Search in Linked ListWe now return to the method f ind defined in Example 6.5:f ind :: if val = 0then return := thiselse if next 6= nullthen next.f indelse return := nullfifiwhere val is an instance integer variable, next is an instance object variable,and return is a normal object variable used to store the result of the method.In order to reason about this method we introduce a normal array variablea of type integer → object such that the section a[k : n] stores a linked listof objects, as expressed by∀ i ∈ [k : n − 1] : a[i].next = a[i + 1].Partial CorrectnessWe first prove that upon termination the call this.f ind returns in the variablereturn the first object which can be reached from this that stores zero, ifthere exists such an object and otherwise return = null.
To this end, weintroduce the assertion p defined byp ≡ y = a[k] ∧ a[n] = return ∧∀ i ∈ [k : n − 1] : (a[i] 6= null ∧ a[i].val 6= 0 ∧ a[i].next = a[i + 1]),where y is a normal object variable and k and n are normal integer variables.The variable y is used as a generic representation of the caller of the methodf ind. The assertion p states that the section a[k : n] stores a linked list of6.8 Case Study: Zero Search in Linked List227objects which starts with the object y, ends with return, and all its objects,except possibly the last one, are different from null and do not store zero.We prove{true} this.f ind {q[y := this]},where q is defined byq ≡ (return = null ∨ return.val = 0) ∧ ∃ a : ∃ k : ∃ n ≥ k : p.The postcondition q thus states that the returned object is null or storeszero and that for some array section a[k : n] the above assertion p holds.We establish a more general correctness formula, namely{true} y.f ind {q}.from which the desired formula follows by the instantiation II rule.By the recursion V rule it suffices to prove{true} y.f ind {q} ⊢ {true} begin local this := y; S end {q},where S denotes the body of the method f ind and ⊢ refers to the proofsystem POP with the recursion VII rule omitted.We present the proof in the form of a proof outline that we give in Figure 6.4.To justify this proof outline it suffices to establish the following threeclaims.Claim 1.
{this = y ∧ val = 0} return := this {q}.Proof. We show(this = y ∧ val = 0) → q[return := this],from which the claim follows by the assignment axiom for normal variablesand the consequence rule.First, since val is an instance variable, we haveval = 0 → this.val = 0,which takes care of the first conjunct of q[return := this].Next, to satisfy the second conjunct of q[return := this] under the assumption this = y, it suffices to take array a such that a[k] = y and n = k.Indeed, we then have both y = a[k] and a[n] = this and the third conjunctof p[return := this] vacuously holds since we then have k > n − 1.⊓⊔Claim 2.{true} y.f ind {q} ⊢ {this = y ∧ val 6= 0 ∧ next 6= null} next.f ind {q}.2286 Object-Oriented Programs{true}begin local{true}this := y;{this = y}if val = 0then{this = y ∧ val = 0}return := this{q}else{this = y ∧ val 6= 0}if next 6= nullthen{this = y ∧ val 6= 0 ∧ next 6= null}next.f ind{q}else{this = y ∧ val 6= 0 ∧ next = null}return := null{q}fi{q}fi{q}end{q}Fig.
6.4 Proof outline showing partial correctness of the f ind method.Proof. We first apply the instantiation II rule to the assumption and obtain{true} next.f ind {q[y := next]}.Next, applying the invariance rule we obtain{this = y ∧ val 6= 0 ∧ next 6= null}next.f ind{q[y := next] ∧ this = y ∧ val 6= 0 ∧ next 6= null}.Now, observe that(q[y := next] ∧ this = y ∧ val 6= 0 ∧ next 6= null) → q.6.8 Case Study: Zero Search in Linked List229Indeed, the first conjunct of q[y := next] and q are identical. Further,assuming q[y := next] ∧ this = y ∧ val 6= 0 ∧ next 6= null we first takethe array section a[k : n] which ensures the truth of the second conjunct ofq[y := next].
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
