3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 40
Текст из файла (страница 40)
(Translation of Total Correctness Proofs of MethodCalls) Let A be a given set of assumptions about method calls such that for{p′ } S {q ′ } ∈ A we have p′ → s 6= null. IfA ⊢ {p} s.m(t̄) {q}thenΘ(A) ⊢ {Θ(p)} m(Θ(s), Θ(t̄)) {Θ(q)},andΘ(p) → Θ(s) 6= null,where the proofs consist of the applications of the consequence rule, the instantiation rules, and the auxiliary rules A3–A7.Proof.
The proof proceeds by induction on the length of the derivation, seeExercise 6.15.⊓⊔Next, we generalize the above lemmas about method calls to statements.Lemma 6.9. (Translation Correctness Proofs Statements) Let A a beset of assumptions about method calls and {p} S {q} a correctness formulaof an object-oriented statement S such that2166 Object-Oriented ProgramsA ⊢ {p} S {q},where ⊢ either refers to the proof system PW or the proof system TW, bothextended with the block rule, the assignment axiom for instance variables, andthe instantiation rule III.
In case of a total correctness proof we additionallyassume that p′ → s 6= null, for {p′ } s.m(t̄) {q ′ } ∈ A. ThenΘ(A) ⊢ {Θ(p)} Θ(S) {Θ(q)}.Proof. The proof proceeds by induction on the structure of S. We treat themain case of a method call and for the remaining cases we refer to Exercise6.16. Let S ≡ s.m(t̄). We distinguish the following cases:Partial correctness. By the Translation Lemma 6.7 we obtainΘ(A) ⊢ {Θ(p)} m(Θ(s), Θ(t̄)) {Θ(q)},from which by the consequence rule we deriveΘ(A) ⊢ {Θ(p) ∧ Θ(s) 6= null} m(Θ(s), Θ(t̄)) {Θ(q)}.We conclude by the failure rule from Section 3.7Θ(A) ⊢ {Θ(p)} if Θ(s) 6= null → m(Θ(s), Θ(t̄)) fi {Θ(q)}.Total correctness. By the Translation Lemma 6.8 we obtainΘ(A) ⊢ {Θ(p)} m(Θ(s), Θ(t̄)) {Θ(q)}andΘ(p) → Θ(s) 6= null.By the failure rule II from Section 3.7 we concludeΘ(A) ⊢ {Θ(p)} if Θ(s) 6= null → m(Θ(s), Θ(t̄)) fi {Θ(q)}.⊓⊔Finally, we have arrived at the following conclusion.Corollary 6.2. (Translation II) For all correctness formulas {p} S {q},where S is an object-oriented program,(i) if {p} S {q} is derivable in the proof system POP, then{Θ(p)} Θ(S) {Θ(q)} is derivable from PRP,(ii) if {p} S {q} is derivable in the proof system TOP,then {Θ(p)} Θ(S) {Θ(q)} is derivable from TRP.6.7 Object Creation217Proof.
The proof proceeds by an induction on the length of the derivation.The case of an application of the recursion rules VII and VIII is dealt withby the Translation Lemma 6.9, see Exercise 6.17.⊓⊔We can now establish soundness of the considered proof systems.Theorem 6.2. (Soundness of POP and TOP)(i) The proof system POP is sound for partial correctness of object-orientedprograms with parameters.(ii) The proof system TOP is sound for total correctness of object-orientedprograms with parameters.Proof. By the Translation Corollaries 6.1 and 6.2, Soundness Corollary 5.1and Soundness Theorem 5.5.⊓⊔6.7 Object CreationIn this section we introduce and discuss the dynamic creation of objects.
Weextend the set of object-oriented programs with the following statement:S ::= u := new,where u is an object variable and new is a keyword that may not be usedas part of local expressions in the programming language. Informally, theexecution of this statement consists of creating a new object and assigningits identity to the variable u.Example 6.21. Given the method definitionsetnext(u) :: next := u,which sets the instance object variable next, the following method inserts anew element in a list of objects linked by their instance variable next:insert :: begin localz := next;next := new;next.setnext(z)end.More specifically, a call this.insert inserts a new element between the objectthis and the next object in the list denoted by the instance variable next (ofthe current object this).
The local variable z is used to store the old valueof the instance variable next. After the assignment of a new object to this2186 Object-Oriented Programsvariable, the method call next.setnext(z) sets the instance variable next ofthe newly created object to the value of z.⊓⊔Throughout this section we restrict ourselves to pure object-oriented programs in which a local object expression s can only be compared for equality(like in s = t) or appear as an argument of a conditional construct (like inif B then s else t fi).
By definition, in local expressions we do not allow• arrays with arguments of type object,• any constant of type object different from null,• any constant op of a higher type different from equality which involvesobject as an argument or value type.We call local expressions obeying these restrictions pure.Example 6.22. We disallow local expressions a[s1 , .
. . , si , . . . , sn ], where siis an object expression. We do allow for arrays with value type object, e.g.,arrays of type integer → object. As another example, we disallow in localexpressions constants like the identity function id on objects.⊓⊔SemanticsIn order to model the dynamic creation of objects we introduce an instanceBoolean variable created which indicates for each object whether it has beencreated. We do not allow this instance variable to occur in programs. It is onlyused to define the semantics of programs.
In order to allow for unboundedobject creation we require that Dobject is an infinite set, whereas in everystate σ the set of created objects, i.e., those objects o ∈ Dobject for whichσ(o)(created ) = true, is finite.We extend the state update by σ[u := new] which describes an assignmentinvolving as a side-effect the creation of a new object and its default initialization. To describe this default initialization of instance variables of newlycreated objects, we introduce an element init T ∈ DT for every basic type T .We define init object = null and init Boolean = true. Further, let init denotethe local (object) state such that• if v ∈ IV ar is of a basic type T theninit(v) = init T ,• if the value type of an array variable a ∈ IV ar is T and di ∈ DTi fori ∈ {1, .
. . , n} theninit(a)(d1 , . . . , dn ) = init T .6.7 Object Creation219To generate new objects we introduce a function ν such that for every(proper) state σ the object ν(σ) does not exist in σ. Formally, we have forevery (proper) state σν(σ) ∈ Dobject and σ(ν(σ))(created ) = false.The state update σ[u := new] is then defined byσ[o := init][u := o],where o = ν(σ).The operational semantics of an object creation statement is described bythe following rule:(xvi) < u := new, σ >→< E, σ[u := new] >,where u is a (possibly subscripted) object variable.Example 6.23. For a (proper) state σ let O defined byO = {o ∈ Dobject | σ(o)(created ) = true}denote the (finite) set of created objects in σ.
Consider o = ν(σ). Thusσ(o)(created ) = false and o 6∈ O. Given the instance object variable next wehave the following transition:< next := new, σ > → < E, τ > where τ = σ[o := init][next := o] > .Then τ (next) = τ (τ (this))(next) = o, τ (o)(created ) = true andτ (o)(next) = null. The set of created objects in τ is given by O ∪ {o}.⊓⊔AssertionsIn the programming language we can only refer to objects that exist; objectsthat have not been created cannot be referred to and thus do not play a role.We want to reason about programs at the same level of abstraction.
Therefore,we do not allow the instance Boolean variable created to occur in assertions.Further, we restrict the semantics of assertions (as defined in Section 6.3)to states which are consistent. By definition, these are states in which thisand null refer to created objects and all (possibly subscripted) normal objectvariables and all (possibly subscripted) instance object variables of createdobjects also refer to created objects.Example 6.24. Let σ be a consistent (proper) state. We have thatσ(null)(created ) = true and σ(σ(this))(created ) = true. For every nor-2206 Object-Oriented Programsmal object variable x with σ(x) = o we have σ(o)(created ) = true.
Further,for every instance object variable y we have that σ(σ(y))(created ) = true.Note that σ(y) = σ(σ(this))(y). In general, for every global object expressions we have σ(σ(s))(created ) = true. That is, in σ we can only refer to createdobjects.⊓⊔In order to reason about object creation we wish to define a substitutionoperation [x := new], where x ∈ V ar is a simple object variable, such thatσ |= p[x := new] iff σ[x := new] |= pholds for all assertions p and all states σ. However, we cannot simply replacex in p by the keyword new because it is not an expression of the assertionlanguage.
Also, the newly created object does not exist in σ and thus cannotbe referred to in σ, the state prior to its creation. To obtain a simple definitionof p[x := new] by induction on p, we restrict ourselves here to assertions p inwhich object expressions can only be compared for equality or dereferenced,and object expressions do not appear as an argument of any other construct(including the conditional construct).Formally, a global expression in which object expressions s can only becompared for equality (like in s = t) or dereferenced (like in s.x) is calledpure. By definition, in pure global expressions we disallow• arrays with arguments of type object,• any constant of type object different from null,• any constant op of a higher type different from equality which involvesobject as an argument or value type,• conditional object expressions.Note that in contrast to pure local expressions, in pure global expressionswe also disallow object expressions as arguments of a conditional construct,like in if B then x else y fi where x and y are object variables.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
