3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 38
Текст из файла (страница 38)
Given the method definitioninc :: count := count + 1where count is an instance integer variable, we prove the following invarianceproperty{this 6= other ∧ this.count = z} other.inc {this.count = z},6.4 Verification203where z ∈ V ar. To this end, we first prove{u 6= other ∧ u.count = z}begin local this := other; count := count + 1 end{u.count = z},(6.2)where u ∈ V ar is a fresh variable.By the assignment axiom for normal variables, we have{if u = other then count + 1 else u.count fi = z}this := other{if u = this then count + 1 else u.count fi = z}.Further, by the assignment axiom for instance variables we have{(u.count = z)[count := count + 1]} count := count + 1 {u.count = z}.Since u[count := count + 1] ≡ u, we have(u.count = z)[count := count + 1]≡ if u = this then count + 1 else u.count fi = z.Clearly,u 6= other ∧ u.count = z → if u = other then count + 1 else u.count fi = z.So we obtain the above correctness formula (6.2) by an application of thecomposition rule, the consequence rule and, finally, the block rule.We can now apply the recursion V rule.
This way we establish{u 6= other ∧ u.count = z} other.inc {u.count = z}.Finally, using the substitution rule A7 with the substitution u := this weobtain the desired correctness formula.⊓⊔Example 6.13. Given an arbitrary method m (so in particular for the abovemethod inc), we now wish to prove the correctness formula{other = null} other.m {false}in the sense of partial correctness. To this end, it suffices to prove{other = null}begin local this := other; S end{false}where m is defined by m :: S, and apply the recursion V rule.Now, by the assignment axiom for normal variables we have(6.3)2046 Object-Oriented Programs{other = null} this := other {this = null}.But by the new definition of truth of assertions we have [[this = null]] = ∅,i.e.,this = null → falseholds.
By the consequence rule we therefore obtain{other = null} this := other {false}.Further, by the invariance axiom A2 we have{false} S {false},so by the composition rule and the block rule we obtain (6.3).Note that by the substitution rule A7 and the consequence rule this impliesthe correctness formula{true} null.m {false}in the sense of partial correctness.⊓⊔Total CorrectnessWe next introduce the proof system for total correctness. Below, the provability symbol ⊢ refers to the proof system TW augmented with the assignmentaxiom 14, the block rule, the instantiation II rule and the auxiliary rulesA3–A7.In order to prove absence of failures due to calls of a method on null, weproceed as in the failure II rule of Section 3.7 and add similar conditions topremises of the recursion rule.
For proving absence of divergence we proceed inan analogous way as in Chapter 5 in the case of procedures with parameters.This results in the following rule.RULE 17: RECURSION VI{p1 } s1 .m1 {q1 }, . . . , {pn } sn .mn {qn } ⊢ {p} S {q},{p1 ∧ t < z} s1 .m1 {q1 }, . . . , {pn ∧ t < z} sn .mn {qn } ⊢{pi ∧ t = z} begin local this := si ; Si end {qi }, i ∈ {1, . .
., n},pi → si 6= null, i ∈ {1, . . ., n}{p} S {q}6.4 Verification205where mi :: Si ∈ D, for i ∈ {1, . . . , n}, and z is an integer variable that doesnot occur in pi , t, qi and Si for i ∈ {1, . . ., n} and is treated in the proofs asa constant.To prove total correctness of object-oriented programs we use then thefollowing proof system TO :PROOF SYSTEM TO :This system consists of the group of axiomsand rules 1–4, 6, 7, 10, 14, 15, 17, and A3–A7.Thus TO is obtained by extending proof system TW by the block rule, theassignment to instance variables axiom, instantiation II rule, the recursion VIrule, and the auxiliary rules A3–A6.Example 6.14. Given the method inc defined as in Example 6.12, so byinc :: count := count + 1,we now prove the correctness formula{this 6= other ∧ other 6= null ∧ this.count = z} other.inc {this.count = z}in the sense of total correctness.
We already proved in Example 6.12{u 6= other ∧ u.count = z}begin local this := other; count := count + 1 end{u.count = z},and the proof is equally valid in the sense of total correctness. So by theconsequence rule we obtain{u 6= other ∧ other 6= null ∧ u.count = z}begin local this := other; count := count + 1 end{u.count = z}.Because of the form of the precondition we can use the recursion VI ruleto derive{u 6= other ∧ other 6= null ∧ u.count = z} other.inc {u.count = z},from which the desired correctness formula follows by the substitution ruleA7.⊓⊔2066 Object-Oriented Programs6.5 Adding ParametersWe now extend the syntax of the object-oriented programs by allowingparametrized method calls.
To this end, we introduce the following rule:S ::= s.m(t1 , . . . , tn ),where, as before, s is the local object expression and m is a method, andt1 , . . . , tn , are the actual parameters of a basic type. A method is now definedby means of a definitionm(u1 , . . . , un ) :: S,where the formal parameters u1 , . . . , un ∈ V ar are of a basic type. We assumethat n ≥ 0, so that we generalize the case studied so far.As before, a program consists of a main statement and a set D of methoddefinitions, where we stipulate the same restrictions concerning the use ofmethod calls and of the object variable this as in the case of parameterlessmethods.Further, we assume the same restriction as in Chapter 5 in order to avoidname clashes between local variables and global variables.Example 6.15.
Consider an instance variable x and the method setx definedbysetx(u) :: x := u.Then the main statementy.setx(t)sets the value of the instance variable x of the object y to the value of thelocal expression t.⊓⊔Example 6.16. Consider an instance object variable next and the methoddefinitionsetnext(u) :: next := u.Then the main statementx.setnext(next); next := xinserts in this list the object denoted by the object variable x between thecurrent object denoted by this and the next one, denoted by next, see Figures 6.2 and 6.3.⊓⊔6.5 Adding Parameters207Fig.
6.2 A linked list before the object insertion.Fig. 6.3 A linked list after the object insertion.SemanticsThe semantics of a method call with parameters is described by the followingcounterparts of the transitions axioms (xii) and (xiii):(xiv) < s.m(t̄), σ >→< begin local this, ū := s, t̄; S end, σ >where σ(s) 6= null and m(ū) :: S ∈ D,(xv) < s.m(t̄), σ >→< E, fail > where σ(s) = null.Example 6.17. Consider the definition of the method setnext of Example6.16. Assuming that x is a normal variable, σ(this) = o and σ(x) = o′ , wehave the following sequence of transitions:→→→→→< x.setnext(next), σ >< begin local this, u := x, next; next := u end, σ >< this, u := x, next; next := u; this, u := σ(this), σ(u), σ >< next := u; this, u := σ(this), σ(u), σ ′ >< this, u := σ(this), σ(u), σ ′ [next := σ(o)(next)] >< E, σ[o′ := τ [next := σ(o)(next)]] >,where σ ′ denotes the stateσ[this, u := o′ , σ(o)(next)]2086 Object-Oriented Programsand τ = σ(o′ ).
The first transition expands the method call into the corresponding block statement which is entered by the second transition. Thethird transition then initializes the local variables this and u which resultsin the state σ ′ . The assignment next := u is executed next. Note thatσ ′ [next := σ ′ (u)]= {by the definition of σ ′ }σ ′ [next := σ(o)(next)]= {by the definition of state update, σ ′ (this) = o′ and σ ′ (o′ ) = τ }σ ′ [o′ := τ [next := σ(o)(next)]].⊓⊔Partial CorrectnessThe proof rules introduced in the previous section are extended to methodcalls with parameters, analogously to the way we extended in Chapter 5 theproof rules for recursive procedures to recursive procedures with parameters.More specifically, the adjustment of the generic method calls is taken careof by the following proof rule that refers to the set D of the assumed methoddeclarations:RULE 18: INSTANTIATION III{p} y.m(x̄) {q}{p[y, x̄ := s, t̄]} s.m(t̄) {q[y, x̄ := s, t̄]}where y, x̄ is a sequence of simple variables in V ar which do not appear inD and var(s, t̄) ∩ change(D) = ∅.Next, the following proof rule is a modification of the recursion III rulefor procedures with parameters to methods with parameters.
The provabilitysymbol ⊢ refers here to the proof system PW augmented with the assignmentaxiom 14, the block rule, the instantiation III rule and the auxiliary axiomsand rules A2–A7.RULE 19: RECURSION VII{p1 } s1 .m1 (t̄1 ) {q1 }, . . . , {pn } sn .mn (t̄n ) {qn } ⊢ {p} S {q},{p1 } s1 .m1 (t̄1 ) {q1 }, . . .
, {pn } sn .mn (t̄n ) {qn } ⊢{pi } begin local this, ūi := si , t̄i ; Si end {qi }, i ∈ {1, . . ., n}{p} S {q}6.5 Adding Parameters209where mi (ūi ) :: Si ∈ D for i ∈ {1, . . . , n}.To prove partial correctness of object-oriented programs with parameterswe use the following proof system POP :PROOF SYSTEM POP :This system consists of the group of axiomsand rules 1–6, 10, 14, 18, 19, and A2–A7.Thus POP is obtained by extending the proof system PW by the block rule,the assignment to instance variables axiom, the instantiation III rule, therecursion VII rule, and the auxiliary axioms and rules A2–A7.Example 6.18. Consider, as in Example 6.15, an instance variable x and themethod setx defined by setx(u) :: x := u.
We prove the correctness formula{true} y.setx(z) {y.x = z}in the sense of partial correctness. By the recursion VII rule, it suffices toderive the correctness formula{true} begin local this, u := y, z; x := u end {y.x = z}.To prove the last correctness formula we first use the assignment axiom forinstance variables to derive{(y.x = z)[x := u]} x := u {y.x = z},where by the definition of substitution(y.x = z)[x := u] ≡ if y = this then u else y.x fi = z.Finally, by the assignment axiom for normal variables we have{if y = y then z else y.x fi = z}this, u := y, z{if y = this then u else y.x fi = z}.By the composition and the consequence rule we obtain{true} this, u := y, z; x := u {y.x = z}.An application of the block rule concludes the proof.Note that even though the assignment to the variable this does not appearin the considered program, it is crucial in establishing the program correctness.⊓⊔2106 Object-Oriented ProgramsTotal CorrectnessWe conclude the discussion by introducing the following proof rule for totalcorrectness of method calls with parameters.
The provability symbol ⊢ refershere to the proof system TW augmented with the assignment axiom 14, theblock rule, the instantiation III rule and the auxiliary rules A3–A7.RULE 20: RECURSION VIII{p1 } s1 .m1 (ē1 ) {q1 }, . . . , {pn } sn .mn (ēn ) {qn } ⊢ {p} S {q},{p1 ∧ t < z} s1 .m1 (ē1 ) {q1 }, . . . , {pn ∧ t < z} sn .mn (ēn ) {qn } ⊢{pi ∧ t = z} begin local this, ūi := si , ēi ; Si end {qi }, i ∈ {1, .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
