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

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

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

So in the case of the list depicted in Figure6.1 if the current object is the one that stores the value 7, then the method callnext.f ind is the call of the f ind method of the object that stores the value 0.This call is conditional: if next equals null, then the search terminates andthe void reference is returned, through the variable return. We shall returnto this program in Section 6.8, where we shall prove its correctness.Given a set D of method definitions, the set change(S), originally definedin Chapter 4 for the case of normal variables, now also includes the instancevariables that can be modified by S. For example, for the main statement Sin Example 6.3, we have count ∈ change(S), given the declarations of themethods inc and reset.

Note that count is owned by different objects andthat the main statement changes the instance variable count of the objectvariables up and down.6.2 SemanticsIn this section we define the semantics of the introduced object-oriented programs. We first define the semantics of local expressions. This semanticsrequires an extension of the definition of state. Subsequently we introduce arevised definition of an update of a state and provide the transition axiomsconcerned with the newly introduced programming constructs.Semantics of Local ExpressionsThe main difficulty in defining the semantics of local expressions is of coursehow to deal properly with the instance variables. As already mentioned above,each instance variable has a different version (‘instance’) in each object. Conceptually, when defining the semantics of an instance variable u we view it asa variable of the form this.u, where this represents the current object.

So,given a proper state σ and a simple instance variable x we first determine thecurrent object o, which is σ(this). Then we determine the local state of thisobject, which is σ(o), or σ(σ(this)), and subsequently apply this local stateto the considered instance variable x. This means that given a proper state6.2 Semantics193σ the value assigned to the instance variable x is σ(o)(x), or, written out infull, σ(σ(this))(x). This two-step procedure is at the heart of the definitiongiven below.Let an infinite set Dobject of object identities be given. We introduce avalue null ∈ Dobject . So in each proper state a variable of type object equalssome object of Dobject , which can be the null object. A proper state σ nowadditionally assigns to each object o ∈ Dobject its local state σ(o).

In turn,a local state σ(o) of an object o assigns a value of appropriate type to eachinstance variable.So the value of an instance variable x ∈ IV ar of an object o ∈ Dobject isgiven by σ(o)(x) and, as before, the value of x ∈ V ar is given by σ(x).Note that the local state of the current object σ(this) is given byσ(σ(this)).

Further, note that in particular, if an instance variable x is oftype Object, then for each object o ∈ Dobject , σ(o)(x) is either null or anobject o′ ∈ Dobject , whose local state is σ(o′ ), i.e., σ(σ(o)(x)). This application of σ can of course be nested, to get local states of the form σ(σ(σ(o)(x))),etc.

Note that a state σ also assigns a local state σ(null) to the null object.However, as we will see below this local state will never be accessed by anobject-oriented program.Formally, we extend the semantics of expressions S[[s]](σ), given in Section 2.3, by the following clauses:• if s ≡ null thenS[[s]](σ) = null.So the meaning of the void reference (i.e., the constant null) is the nullobject,• if s ≡ x for some simple instance variable x thenS[[s]](σ) = σ(o)(x),where o = σ(this),• if s ≡ a[s1 , . . . , sn ] for some instance array variable a thenS[[s]](σ) = σ(o)(a)(S[[s1 ]](σ), . .

. , S[[sn ]](σ)),where o = σ(this).We abbreviate S[[s]](σ) by σ(s). So for a simple instance variableσ(x) = σ(σ(this))(x).(6.1)1946 Object-Oriented ProgramsUpdates of StatesNext, we proceed with the revision of the definition of a state update for thecase of instance variables. Here, the intuition we provided when explainingthe semantics of instance variables, is of help.

Consider a proper state σ,a simple instance variable x and a value d belonging to the type of x. Toperform the corresponding update of σ on x we first identify the currentobject o, which is σ(this) and its local state, which is σ(o), or σ(σ(this)),that we denote by τ . Then we perform the appropriate update on the stateτ . So the desired update of σ is achieved by modifying τ to τ [x := d].In general, let u be a (possibly subscripted) instance variable of type Tand τ a local state. We define for d ∈ DTτ [u := d]analogously to the definition of state update given in Section 2.3.Furthermore, we define for an object o ∈ Dobject and local state τ , thestate update σ[o := τ ] by½τif o = o′σ[o := τ ](o′ ) =′σ(o ) otherwise.We are now in a position to define the state update σ[u := d] for a (possiblysubscripted) instance variable u of type T and d ∈ DT , as follows:σ[u := d] = σ[o := τ [u := d]],where o = σ(this) and τ = σ(o).

Note that the state update σ[o := τ [u := d]]assigns to the current object o the update τ [u := d] of its local state τ . Inits fully expanded form we get the following difficult to parse definition of astate update:σ[u := d] = σ[σ(this) := σ(σ(this))[u := d]].Example 6.6. Let x be an integer instance variable, o = σ(this), and τ =σ(o). Then=σ[x := 1](x){(6.1) with σ replaced by σ[x := 1]}σ[x := 1](σ[x := 1](this))(x)= {by the definition of state update, σ[x := 1](this) = σ(this) = o}σ[x := 1](o)(x)6.2 Semantics195={definition of state update σ[x := 1]}σ[o := τ [x := 1]](o)(x){definition of state update σ[o := τ [x := 1]]}τ [x := 1](x)= {definition of state update τ [x := 1]}=1.⊓⊔Semantics of Statements and ProgramsTo define the semantics of considered programs we introduce three transition axioms that deal with the assignment to (possibly subscripted) instancevariables and with the method calls.

The first axiom uses the state updatedefined above.(xi) < u := t, σ >→< E, σ[u := σ(t)] >,(xii) < s.m, σ >→< begin local this := s; S end, σ >where σ(s) 6= null and m :: S ∈ D,(xiii) < s.m, σ >→< E, fail > where σ(s) = null.So thanks to the extended definition of a state update, the first transitionaxiom models the meaning of an assignment to an instance variable in exactlythe same way as the meaning of the assignment to a normal variable.The second transition axiom shows that we reduce the semantics of methodcalls to procedure calls with parameters by treating the variable this as aformal parameter and the called object as the corresponding actual parameter.

The third transition axiom shows the difference between the method callsand procedure calls: if in the considered state σ the called object s equals thevoid reference (it equals null), then the method call yields a failure.We could equally well dispense with the use of the block statement in thetransition axiom (xii) by applying to the right configuration the transitionaxiom (ix) for the block statement. The resulting transition axiom wouldthen take the form< s.m, σ >→< this := s; S; this := σ(this), σ >,where σ(s) 6= null and m(ū) :: S ∈ D. Then the variable this would remaina global variable throughout the computation.We did not do this for a number of reasons:1966 Object-Oriented Programs• the proposed axiom captures explicitly the ‘transitory’ change of the valueof the variable this,• in the new recursion rule that deals with the method calls we do need theblock statement anyway,• later we shall need the block statement anyway, to define the meaning ofthe calls of methods with parameters.Example 6.7.

Given the method getx defined in Example 6.2 and an objectvariable y, we obtain the following computation:→→→→→< y.getx, σ >< begin local this := y; return := x end, σ >< this := y; return := x; this := σ(this), σ >< return := x; this := σ(this), σ[this := σ(y)] >{see simplification 1 below}< this := σ(this), σ[this := σ(y)][return := σ(σ(y))(x)] >{see simplication 2 below}< E, σ[return := σ(σ(y))(x)] > .In the last two transitions we performed the following simplifications in configurations on the right-hand side.Re: 1.σ[this := σ(y)](x){(6.1) with σ replaced by σ[this := σ(y)]}σ[this := σ(y)](σ[this := σ(y)](this))(x)= {by the definition state update, σ[this := σ(y)](this) = σ(y)}==σ[this := σ(y)](σ(y))(x){by the definition state update, σ[this := σ(y)](σ(y)) = σ(σ(y))}σ(σ(y))(x)Re: 2.==σ[this := σ(y)][return := σ(σ(y))(x)][this := σ(this)]{since return 6≡ this}σ[return := σ(σ(y))(x)][this := σ(y)][this := σ(this)]{the last update overrides the second updateby the value this has in σ}σ[return := σ(σ(y))(x)]This completes the calculation of the computation.⊓⊔6.3 Assertions197Lemma 6.1.

(Absence of Blocking) For every S that can arise during anexecution of an object-oriented program, if S 6≡ E then for any proper stateσ, such that σ(this) 6= null, there exists a configuration < S1 , τ > such that< S, σ > → < S1 , τ >,where τ (this) 6= null.Proof. If S 6≡ E then any configuration < S, σ > has a successor in thetransition relation → .

To prove the preservation of the assumed propertyof the state it suffices to consider the execution of the this := s assignment.Each such assignment arises only within the context of the block statement inthe transition axiom (xii) and is activated in a state σ such that σ(s) 6= null.This yields a state τ such that τ (this) 6= null.⊓⊔When considering verification of object-oriented programs we shall onlyconsider computations that start in a proper state σ such that σ(this) 6= null,i.e., in a state in which the current object differs from the void reference. TheAbsence of Blocking Lemma 6.1 implies that such computations never leadto a proper state in which this inequality is violated.The partial correctness semantics is defined exactly as in the case of therecursive programs with parameters considered in Chapter 5.

(Recall that weassumed a given set D of method declarations.)The total correctness semantics additionally records failures. So, as in thecase of the failure admitting programs from Section 3.7, we have for a properstate σMtot [[S]](σ) =M[[S]](σ)∪ {⊥ | S can diverge from σ}∪ {fail | S can fail from σ}.Example 6.8.

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

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