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

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

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

Let us return to Example 6.2. On the account of Example 6.7the following holds for the object variable y:• if σ(y) 6= null thenM[[y.getx]](σ) = Mtot [[y.getx]](σ) = {σ[return := σ(σ(y))(x)]},• if σ(y) = null thenM[[y.getx]](σ) = ∅ and Mtot [[y.getx]](σ) = {fail}.⊓⊔6.3 AssertionsLocal expressions of the programming language only refer to the local stateof the executing object and do not allow us to distinguish between differ-1986 Object-Oriented Programsent versions of the instance variables. In the assertions we need to be moreexplicit.

So we introduce the set of global expressions which extends the setof local expressions introduced in Subsection 6.1 by the following additionalclauses:• if s is a global expression of type object and x is an instance variable ofa basic type T then s.x is a global expression of type T ,• if s is a global expression of type object, s1 , . .

. , sn are global expressionsof type T1 , . . . , Tn , and a is an array instance variable of type T1 ×. . .×T1 →T then s.a[s1 , . . . , sn ] is a global expression of type T .In particular, every local expression is also a global expression.Example 6.9. Consider a normal integer variable i, a normal variable x oftype object, a normal array variable of type integer → object, and aninstance variable next of type object.Using them and the normal this variable (that is of type object) we cangenerate the following global expressions:••••next, next.next, etc.,this.next, this.next.next, etc.,x.next, x.next.next, etc.,a[i].next,all of type object. In contrast, next.this and next.x are not global expressions, since neither this nor x are instance variables.⊓⊔We call a global expression of the form s.u a navigation expression sinceit allows one to navigate through the local states of the objects. For example,the global expression next.next refers to the object that can be reached by‘moving’ to the object denoted by the value of next of the current object thisand evaluate the value of its variable next.We define the semantics of global expressions as follows:• for a simple instance variable x of type T ,S[[s.x]](σ) = σ(o)(x),where S[[s]](σ) = o,• for an instance array variable a with value type TS[[s.a[s1 , .

. . , sn ]]](σ) = σ(o)(a)(S[[s1 ]](σ), . . ., S[[sn ]](σ)),where S[[s]](σ) = o.We abbreviate S[[t]](σ) by σ(t).So for a (simple or subscripted) instance variable u the semantics of u andthis.u coincide, that is, for all proper states σ we have σ(u) = σ(this.u). In6.3 Assertions199other words, we can view an instance variable u as an abbreviation for theglobal expression this.u.Note that this semantics also provides meaning to global expressions ofthe form null.u.

However, such expressions are meaningless when specifyingcorrectness of programs because the local state of the null object can never bereached in computations starting in a proper state σ such that σ(this) 6= null(see the Absence of Blocking Lemma 6.1).Example 6.10. If x is an object variable and σ a proper state such thatσ(x) 6= null, then for all simple instance variables yσ(x.y) = σ(σ(x))(y).⊓⊔Assertions are constructed from global Boolean expressions as in Section 2.5. This means that only normal variables can be quantified.SubstitutionThe substitution operation [u := t] was defined in Section 2.7 only for thenormal variables u and for the expressions and assertions as defined there.We now extend the definition to the case of instance variables u and globalexpressions and assertions constructed from them.Let u be a (simple or subscripted) instance variable and s and t global expressions.

In general, the substitution [u := t] replaces every possible alias e.uof u by t. In addition to the possible aliases of subscripted variables, we nowalso have to consider the possibility that the global expression e[u := t] denotes the current object this. This explains the use of conditional expressionsbelow.Here are the main cases of the definition substitution operation s[u := t]:• if s ≡ x ∈ V ar thens[u := t] ≡ x• if s ≡ e.u and u is a simple instance variable thens[u := t] ≡ if e′ = this then t else e′ .u fiwhere e′ ≡ e[u := t],• if s ≡ e.a[s1 , .

. . , sn ] and u ≡ a[t1 , . . . , tn ] thenVns[u := t] ≡ if e′ = this ∧ i=1 s′i = ti then t else e′ .a[s′1 , . . . , s′n ] fiwhere e′ ≡ e[u := t] and s′i ≡ si [u := t] for i ∈ {1, . . . , n}.2006 Object-Oriented ProgramsThe following example should clarify this definition.Example 6.11. Suppose that s ≡ this.u. Thenthis.u[u := t]≡ if this[u := t] = this then t else .

. . fi≡ if this = this then t else . . . fi.So this.u[u := t] and t are equal, i.e., for all proper states σ we haveσ(this.u[u := t]) = σ(t).Next, suppose that s ≡ this.a[x], where x is a simple variable. Thenthis.a[x][a[x] := t]≡ if this[a[x] := t] = this ∧ x[a[x] := t] = x then t else . . . fi≡ if this = this ∧ x = x then t else . . . fi.So this.a[x][a[x] := t] and t are equal.Finally, for a simple instance variable u and a normal object variable x wehavex.u[u := t]≡ if x[u := t] = this then t else x[u := t].u fi≡ if x = this then t else x.u fi.⊓⊔The substitution operation is then extended to assertions in the same wayas in Section 2.5 and the semantics of assertions is defined as in Section 2.6.We have the following counterpart of the Substitution Lemma 2.4.Lemma 6.2.

(Substitution of Instance Variables) For all global expressions s and t, all assertions p, all simple or subscripted instance variables uof the same type as t and all proper states σ,(i) σ(s[u := t]) = σ[u := σ(t)](s),(ii) σ |= p[u := t] iff σ[u := σ(t)] |= p.Proof. See Exercise 6.3.⊓⊔6.4 VerificationWe now study partial and total correctness of object-oriented programs.

Tothis end, we provide a new definition of a meaning of an assertion, now definedby6.4 Verification201[[p]] = {σ | σ is a proper state such that σ(this) 6= null and σ |= p},and say that an assertion p is is true, or holds, if[[p]] = {σ | σ is a proper state such that σ(this) 6= null}.This new definition ensures that when studying program correctness we limitourselves to meaningful computations of object-oriented programs.The correctness notions are then defined in the familiar way using thesemantics M and Mtot . In particular, total correctness is defined by:|=tot {p} S {q} if Mtot [[S]]([[p]]) ⊆ [[q]].Since by definition fail, ⊥ 6∈ [[q]] holds, as in the case of the failure admittingprograms from Section 3.7, |=tot {p} S {q} implies that S neither fails nordiverges when started in a proper state σ satisfying p and such thatσ(this) 6= null.Partial CorrectnessWe begin, as usual, with partial correctness.

We have the following axiom forassignments to (possibly subscripted) instance variables.AXIOM 14: ASSIGNMENT TO INSTANCE VARIABLES{p[u := t]} u := t {p}where u is a (possibly subscripted) instance variable.So this axiom uses the new substitution operation defined in the sectionabove.To adjust the correctness formulas that deal with generic method calls tospecific objects we modify the instantiation rule 11 of Section 5.3 as follows.We refer here to the given set D of method declarations.RULE 15: INSTANTIATION II{p} y.m {q}{p[y := s]} s.m {q[y := s]}where y 6∈ var(D) and var(s) ∩ change(D) = ∅.The recursion III rule for partial correctness of recursive procedure callswith parameters that we introduced in Chapter 5 can be readily modifiedto deal with the method calls.

To this end, it suffices to treat the variablethis as a formal parameter of every method definition and the callee of a2026 Object-Oriented Programsmethod call as the corresponding actual parameter. This yields the followingproof rule that deals with partial correctness of recursive methods. Belowthe provability symbol ⊢ refers to the proof system PW augmented withthe assignment axiom 14, the block rule, the instantiation II rule and theauxiliary axioms and rules A2–A7.RULE 16: RECURSION V{p1 } s1 .m1 {q1 }, .

. . , {pn } sn .mn {qn } ⊢ {p} S {q},{p1 } s1 .m1 {q1 }, . . . , {pn } sn .mn {qn } ⊢{pi } begin local this := si ; Si end {qi }, i ∈ {1, . . ., n}{p} S {q}where mi :: Si ∈ D, for i ∈ {1, . . ., n}.To prove partial correctness of object-oriented programs we use the following proof system PO:PROOF SYSTEM PO :This system consists of the group of axiomsand rules 1–6, 10, 14–16, and A2–A7.We assume here and in the other proof systems presented in this chapterthat the substitution rule A7 and the ∃-introduction rule A5 refer to thenormal variables, i.e., we cannot substitute or eliminate instance variables.Thus PO is obtained by extending the proof system PW by the blockrule, the assignment to instance variables axiom, the instantiation II rule,the recursion V rule, and the auxiliary axioms and rules A2–A7.When we deal only with one, non-recursive method and use the methodcall as the considered program, the recursion V rule can be simplified to{p} begin local this := s; S end {q}{p} s.m {q}where D = m :: S.We now illustrate the above proof system by two examples in which weuse this simplified version of the recursion V rule.Example 6.12.

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

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