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

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

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

In Section 6.5 we discuss the extension to method calls withparameters. In Section 6.6 we introduce a transformation of object-orientedprograms into recursive programs and use it to prove soundness of the proofsystems introduced for reasoning about object-oriented programs.Next, in Section 6.7 we introduce a new assignment axiom for object creation. Finally, in Section 6.8 we prove as a case study the correctness of anobject-oriented program that implements a search for zero in a linked listof integers, and in Section 6.9 the correctness of an object-oriented programthat inserts a new object in a linked list.6.1 Syntax1876.1 SyntaxWe first describe the syntax of the expressions of the considered programminglanguage and then define the syntax of method calls, method definitions andobject-oriented programs.Local ExpressionsThe set of expressions used here extends the set of expressions introduced inSection 2.2.

We call them local expressions to stress that they refer to localproperties of objects. We begin by introducing a new basic type object whichdenotes the set of objects. A local expression (e.g, a variable) of type objectdenotes an object. Simple variables of type object and array variables withvalue type object are called object variables. As a specific case, we distinguishthe simple object variable this which at each state denotes the currentlyexecuting object.Recall from Section 2.2 that we denote the set of all simple and arrayvariables by Var.

We now introduce a new set IV ar of instance variables(so V ar ∩ IV ar = ∅). An instance variable is a simple variable or an arrayvariable. Thus we now have two kinds of variables: the up till now considerednormal variables (V ar), which are shared, and instance variables (IV ar),which are owned by objects.

Each object has its own local state which assignsvalues to the instance variables. We stipulate that this is a normal variable,that is, this ∈ V ar.The only operation of a higher type which involves the basic type object(as argument type or as value type) is the equality =object (abbreviated by=).

Further, as before we abbreviate ¬(s = t) by s 6= t. Finally, the constantnull of type object represents the void reference, a special construct whichdoes not have a local state.Example 6.1. Given an array variable a ∈ V ar ∪ IV ar of typeinteger → object,• a[0] is a local expression of type object,• this = a[0] and this 6= null are local Boolean expressions.⊓⊔Summarizing, the set of expressions defined in Section 2.2 is extended bythe introduction of the basic type object, the constant null of type object,and the set IV ar of (simple and array) instance variables.

Local object expressions, i.e., expressions of type object, can only be compared for equality.A variable is either a normal variable (in V ar) or an instance variable (inIV ar). Simple variables (in V ar ∪IV ar) can now be of type object. Also the1886 Object-Oriented Programsargument and the value types of array variables (in V ar ∪ IV ar) can be oftype object. Finally, we have the distinguished normal object variable this.Statements and ProgramsWe extend the definition of statements given in Section 3.1 with block statements, as introduced in Section 5.1, and method calls which are described bythe following clause:S ::= s.m.The local object expression s in the method call s.m denotes the called object.The identifier m denotes a method which is a special kind of procedure.The methods are defined as parameterless procedures, by means of a definitionm :: S.Here S is the method body.

Because the statements now include method calls,we allow for recursive (albeit parameterless) methods. The instance variablesappearing in the body S of a method definition are owned by the executing object which is denoted by the variable this. To ensure correct use ofthe variable this, we only consider statements in which this is read-only,that is, we disallow assignments to the variable this.

Further, to ensure thatinstance variables are permanent, we require that in each block statementbegin local ū := t̄; S end we have var(ū) ⊆ V ar \ {this}, that is, instancevariables are not used as local variables. However, when describing the semantics of method calls, we do use ‘auxiliary’ block statements in which thevariable this is used as a local variable (see the discussion in Example 6.2),so in particular, it is initialized (and hence modified).Apart from denoting the callee of a method call, local object expressions,as already indicated in Example 6.1, can appear in local Boolean expressions.

Further, we allow for assignments to object variables. In particular,the assignment u := null is used to assign to the object variable u the voidreference, which is useful in programs concerned with dynamic data structures (such as lists), see Example 6.5. In turn, the assignment u := v for theobject variables u and v causes u and v to point to the same object. Particularly useful is the assignment of the form x := this that causes x to pointto the currently executing object. An example will be given below.We now denote by D a set of method definitions. Object-oriented programsconsist of a main statement S and a given set D of method definitions suchthat each method used has a unique declaration in D and each method callrefers to a method declared in D. Finally, we assume that the name clashesbetween local variables and global variables are resolved in the same way asin Chapter 5, so by assuming that no local variable of S occurs in D.From now on we assume a given set D of method definitions.6.1 Syntax189Example 6.2.

Suppose that the set D contains the method definitiongetx :: return := x,where return ∈ V ar and x ∈ IV ar. Then the method cally.getx,where y ∈ V ar ∪ IV ar is an object variable, assigns the value of the instancevariable x of the called object denoted by y to the normal variable return. Theexecution of this method call by the current object, denoted by this, transferscontrol from the local state of the current object to that of the called objecty.

Semantically, this control transfer is described by the (implicit) assignmentthis := y,which sets the current executing object to the one denoted by y. After theexecution of the method body control is transferred back to the calling objectwhich is denoted by the previous value of this. Summarizing, the executionof a method call y.getx can be described by the block statementbegin local this := y; return := x end.Because of the assignment this := y, the instance variable x is owned withinthis block statement by the called object y.

Note that upon termination thelocal variable this is indeed reset to its previous value (which denotes thecalling object).Consider now the main statementy.getx; z := return.Using the method call y.getx it assigns to the instance variable z of thecurrent object the value of the instance variable x of the object denoted byy, using the variable return.The names of the instance variables can coincide. In case x ≡ z, the abovemain statement copies the value of the instance variable x owned by y to theinstance variable x of the current object, denoted by this.⊓⊔Example 6.3. Given an instance integer variable count we define the methods inc and reset as follows:inc :: count := count + 1,reset :: count := 0.Assume now normal integer variables i, j and n, normal object variablesup and down and a normal array variable a of type integer → integer.

Themain statement1906 Object-Oriented Programsi := 0;up.reset;down.reset;while i ≤ ndo if a[i] > jthen up.incelse if a[i] < k then down.inc fifi;i := i + 1odcomputes the number of integers greater than j and the number of integerssmaller than k, stored in a[0 : n], using two normal object variables up anddown. Since count is an instance variable, the call up.inc of the method incof up does not affect the value of count of the object down (and vice versa),assuming up 6= down, i.e., when up and down refer to distinct objects.⊓⊔The above example illustrates one of the main features of instance variables. Even though there is here only one variable count, during the programexecution two instances (hence the terminology of an ‘instance variable’) ofthis variable are created and maintained: up.count and down.count.

Whenthe control is within the up object (that is, up is the currently executing object), then up.count is used, and when the control is within the down object,then down.count is used.The next two examples illustrate the important role played by the instanceobject variables. They allow us to construct dynamic data structures, likelists.Example 6.4. We represent a (non-circular) linked list using the instanceobject variable next that links the objects of the list, and the constant nullthat allows us to identify the last element of the list. We assume that eachobject stores a value, kept in an instance integer variable val.

Additionally,we use the normal object variable f irst to denote (point to) the first objectin the list, see for example Figure 6.1.Fig. 6.1 A list.6.1 Syntax191We want to compute the sum of the instance variables val. To this end,we additionally use the normal integer variable sum, normal object variablecurrent that (points to) denotes the current object, and two methods, addand move, defined as follows:add :: sum := sum + val,move :: current := next.The first one updates the variable sum, while the second one allows us toprogress to the next object in the list.The following main statement then computes the desired sum:sum := 0;current := f irst;while current 6= null do current.add; current.move od.⊓⊔In this example the method call current.move is used to ‘advance’ thevariable current to point to the next element of the list.

Note that this effectof advancing the variable current cannot be achieved by using the assignmentcurrent := next instead. Indeed, the repeated executions of the assignmentcurrent := next can modify the variable current only once.The next example presents a program that uses a recursive method.Example 6.5. Consider again a non-circular linked list built using an instance object variable next and the constant null, representing the last element, such as the one depicted in Figure 6.1. Then, given an integer instancevariable val and a normal object variable return, the following recursivemethodf ind :: if val = 0then return := thiselse if next 6= nullthen next.f indelse return := nullfifireturns upon termination of the call this.f ind an object that stores zero.More precisely, if such an object exists, then upon termination the variablereturn points to the first object in the list that stores zero and otherwise thevoid reference (represented by the constant null) is returned.⊓⊔This program is a typical example of recursion over dynamic data structures represented by objects.

The recursive call of the method f ind of theobject denoted by the instance variable next involves a transfer of the control from the local state of the calling object this to the local state of the1926 Object-Oriented Programsnext object in the list. Since the variable next is an instance variable, whichversion of it is being referred to and which value it has depends on whichobject is currently executing.More specifically, in the example list depicted in Figure 6.1 the call of themethod f ind on the first object, i.e., one that stores the value 7, searches forthe first object whose val variable equals zero. If such an object is found, it isreturned using the object variable this. Note that the outer else branch leadsto the call next.f ind of the f ind method of the object to which the variablenext of the current object refers.

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

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