3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 39
Текст из файла (страница 39)
. ., n}pi → si 6= null, i ∈ {1, . . ., n}{p} S {q}where mi (ūi ) :: Si ∈ D, for i ∈ {1, . . . , n}, and z is an integer variable thatdoes not occur in pi , t, qi and Si for i ∈ {1, . . ., n} and is treated in the proofsas a constant.To prove total correctness of object-oriented programs with parameters weuse the following proof system TOP :PROOF SYSTEM TOP :This system consists of the group of axiomsand rules 1–4, 6, 7, 10, 14, 18, 20, and A3–A7.Thus TOP is obtained by extending the proof system TW by the block rule,the assignment to instance variables axiom, the instantiation III rule, therecursion VIII rule, and the auxiliary rules A3–A7.Example 6.19. Given the method setx defined as in Example 6.15 we nowprove the correctness formula{y 6= null} y.setx(z) {y.x = z}in the sense of total correctness.We already proved in Example 6.18{true} begin local this, u := y, z; x := u end {y.x = z}and the proof is equally valid in the sense of total correctness.
So by theconsequence rule we obtain{y 6= null} begin local this, u := y, z; x := u end {y.x = z}.6.6 Transformation of Object-Oriented Programs211Because of the form of the precondition we can now derive the desiredcorrectness formula using the recursion VIII rule.⊓⊔6.6 Transformation of Object-Oriented ProgramsThe proof rules for reasoning about the correctness of object-oriented programs (with parameters) are derived from the corresponding proof rules forrecursive programs of Chapter 5. In this section we define the underlyingtransformation of object-oriented programs (with parameters) into recursiveprograms augmented by the failure statement from Section 3.7.
This statement is needed to take care of the method calls on the void reference. Weprove then that this transformation preserves both partial and total correctness and use this fact to prove soundness of the introduced proof systems.First we transform instance variables into normal array variables.
For example, an instance variable x of a basic type T is transformed into a normalarray variable x of typeobject → T.The normal array variable x stores for each object the value of its instancevariable x. Similarly, an instance array variable a of type T1 × . .
. × Tn → Tis transformed into a normal array variable a of typeobject × T1 × . . . × Tn → T.Then for every state σ we denote by Θ(σ) the corresponding ‘normal’ state (asdefined in Section 2.3) which represents the instance variables as (additional)normal variables. We have• Θ(σ)(x) = σ(x), for every normal variable x,• Θ(σ)(x)(o) = σ(o)(x), for every object o ∈ Dobject and normal arrayvariable x of type object → T being the translation of an instance variablex of a basic type T ,• Θ(σ)(a)(o, d1 , .
. . , dn ) = σ(o)(a)(d1 , . . . , dn ), for every object o ∈ Dobjectand normal array variable a of type object × T1 × . . . × Tn → T being thetranslation of an instance array variable a of type T1 × . . . × Tn → T , anddi ∈ DTi , for i ∈ {1, . . . , n}.Next we define for every local expression s of the object-oriented programming language the normal expression Θ(s) by induction on the structure ofs. We have the following basic cases.• Θ(x) ≡ x, for every normal variable x,• Θ(x) ≡ x[this], for every instance variable x of a basic type,• Θ(a[s1 , .
. . , sn ]) ≡ a[this, Θ(s1 ), . . . , Θ(sn )], for every instance array variable a.2126 Object-Oriented ProgramsThe following lemma clarifies the outcome of this transformation.Lemma 6.3. (Translation) For all proper states σ(i) for all local expressions sS[[s]](σ) = S[[Θ(s)]](Θ(σ)),where S[[Θ(s)]](Θ(σ)) refers to the semantics of expressions defined inSection 2.3,(ii) for all (possibly subscripted) instance variables u and values d of thesame type as uσ[u := d] = Θ(σ)[Θ(u) := d].Proof. The proof proceeds by a straightforward induction on the structureof s and case analysis of u, see Exercise 6.9.⊓⊔Next, we extend Θ to statements of the considered object-oriented language, by induction on the structure of the statements.• Θ(u := s) ≡ Θ(u) := Θ(s),• Θ(s.m(s1 , . . .
, sn )) ≡ if Θ(s) 6= null → m(Θ(s), Θ(s1 ), . . . , Θ(sn )) fi,• Θ(S1 ; S2 ) ≡ Θ(S1 ); Θ(S2 ),• Θ(if B then S1 else S2 fi) ≡ if Θ(B) then Θ(S1 ) else Θ(S2 ) fi,• Θ(while B do S od) ≡ while Θ(B) do Θ(S) od,• Θ(begin local ū := t̄; S end) ≡ begin local ū := Θ(t̄); Θ(S) end,where Θ(t̄) denotes the result of applying to the expressions of t̄.So the translation of a method call transforms the called object s into anadditional actual parameter of a call of the procedure m.
Additionally a checkfor a failure is made. Consequently, we transform every method definitionm(u1 , . . . , un ) :: Sinto a procedure declarationm(this, u1 , . . . , un ) :: Θ(S),which transforms the distinguished normal variable this into an additionalformal parameter of the procedure m. This way the set D of method definitions is transformed into the setΘ(D) = {m(this, u1 , .
. . , un ) :: Θ(S) | m(u1 , . . . , un ) :: S ∈ D}of the corresponding procedure declarations.We establish the correspondence between an object-oriented program Sand its transformation Θ(S) using an alternative semantics of the recursive6.6 Transformation of Object-Oriented Programs213programs augmented by the failure statement. This way we obtain a precisematch between S and Θ(S). This alternative semantics is defined using anew transition relation ⇒ for configurations involving recursive programsaugmented by the failure statement, defined as follows:< S, σ > → < S ′ , τ >where S is not a failure statement,< S, σ >⇒< S ′ , τ >< S, σ >⇒< S ′ , τ >2.where σ |= b,< if B → S fi, σ >⇒< S ′ , τ >3.
< if B → S fi, σ >⇒< E, fail > where σ |= ¬b.1.So in the transition relation ⇒ a successful transition of a failure statementconsists of a transition of its main body, i.e., the successful evaluation of theBoolean guard itself does not give rise to a transition.Example 6.20. Let σ(x) = 2 and σ(z) = 4. We have< if x 6= 0 → y := z div x fi, σ >⇒< E, σ[y := 2] >,whereas< if x 6= 0 → y := z div x fi, σ >→ < y := z div x, σ >→ < E, σ[y := 2] > .⊓⊔We have the following correspondence between the two semantics.Lemma 6.4. (Correspondence) For all recursive programs S augmentedby the failure statement, all proper states σ, and all proper or fail states τ< S, σ >→∗ < E, τ > iff < S, σ >⇒∗ < E, τ > .Proof. The proof proceeds by induction on the number of transitions, seeExercise 6.10.⊓⊔Further, we have the following correspondence between an object-orientedprogram S and its transformation Θ(S).Lemma 6.5.
(Transformation) For all object-oriented programs S, allproper states σ, and all proper or fail states τ< S, σ >→< E, τ > iff < Θ(S), Θ(σ) >→< e, Θ(τ ) >,where τ is either a proper state or fail.Proof. The proof proceeds by induction on the structure of S, see Exercise6.11.⊓⊔2146 Object-Oriented ProgramsThe following theorem then states the correctness of the transformationΘ.Theorem 6.1. (Correctness of Θ) For all object-oriented programs S (witha set of method declarations D) and proper states σ(i) Θ(M[[S]](σ)) = M[[Θ(S)]](Θ(σ)),(ii) Θ(Mtot [[S]](σ)) = Mtot [[Θ(S)]](Θ(σ)),where the given set D of method declarations is transformed into Θ(D).Proof. The proof combines the Correspondence Lemma 6.4 and the Transformation Lemma 6.5, see Exercise 6.12.⊓⊔SoundnessGiven the above transformation, soundness of the proof systems for partialand total correctness of object-oriented programs can be reduced to soundnessof the corresponding proof systems for recursive programs augmented by thefailure statement.
For this reduction we also have to transform expressionsof the assertion language. For every global expression e we define Θ(e) byinduction on the structure of e, assuming the above transformation of instancevariables. We have the following main case of navigation expressions:Θ(e.x) = x[Θ(e)].The transformation Θ(e) is extended to a transformation Θ(p) of assertionsby a straightforward induction on the structure of p. Correctness of this transformation of assertions is stated in the following lemma. For the assertionsintroduced in this chapter we use a more restrictive meaning, so only animplication holds here.Lemma 6.6. (Assertion) For all assertions p and proper states σσ |= p iff Θ(σ) |= Θ(p).Proof. The proof proceeds by induction on the structure of p, see Exercise6.13.⊓⊔Corollary 6.1.
(Translation I) For all correctness formulas {p} S {q},where S is an object-oriented program,if |= {Θ(p)} Θ(S) {Θ(q)} then |= {p} S {q},andif |=tot {Θ(p)} Θ(S) {Θ(q)} then |=tot {p} S {q}.6.6 Transformation of Object-Oriented Programs215Proof. It follows directly by the Assertion Lemma 6.6 and the CorrectnessTheorem 6.1.⊓⊔Finally, we show that a correctness proof of an object-oriented program canbe translated to a correctness proof of the corresponding recursive program.We need the following lemmas which state that (partial and total) correctnessproofs of a method call from a given set of assumptions can be translated tocorrectness proofs of the corresponding procedure call from the correspondingset of assumptions.
For a given set of assumptions A about method calls, wedefine the set of assumptions Θ(A) about the corresponding procedure callsby{Θ(p)} m(Θ(s), Θ(t̄)) {Θ(q)} ∈ Θ(A) iff {p} s.m(t̄) {q} ∈ A.Lemma 6.7. (Translation of Partial Correctness Proofs of MethodCalls) Let A be a given set of assumptions about method calls. IfA ⊢ {p} s.m(t̄) {q},thenΘ(A) ⊢ {Θ(p)} m(Θ(s), Θ(t̄)) {Θ(q)},where the proofs consist of the applications of the consequence rule, the instantiation rules, and the auxiliary axioms and rules A2–A7.Proof. The proof proceeds by induction on the length of the derivation, seeExercise 6.14.⊓⊔Lemma 6.8.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
