(which is needed for technical reasons), an elementary statement s (as defined above), a sequential composition statement, a conditional statement and an iteration statement, similar to that in the previous section. The transition rules for elementary statements are given in slide 10-rules.

Assignment

rules

$<< v = e, %f^{%a} >> -> << %e, %f [ %a.v := e_{%f} ] >>$

Object creation

\ffrac{ $<< S_{%t}, %f^{%a} >> \apijl{%l} << %e, %f' >>$ }{ $<< x \! = \! new %t, %f >> \! \apijl{ %a \. %l } \! << %e , %f'[ x \! := %a \! ]>>$ }

Method call

\ffrac{ $<< S_m(e), %f^{%a} >> \apijl{%l} << %e, %f' >>$ }{ $<< x.m(e), %f >> \apijl{ m_{%a} \. %l } << %e, %f' >>$ }

slide: Transition system -- rules

The assignment rule states that the assignment of (the value of) an expression e to a (local) variable v in state

%f

decorated by an object identifier

%a

results in the empty statement and the state

%f

modified by assigning the value of e in

%f

(which is written as

e_{%f}

) to the instance variable v of object

%a

. Hence, decorations allow us to work in the local environment of the object indicated by the decoration. The object creation rule states that if we assume a transition

<< S_{%t}, %f^{%a} >> \apijl{%l} << %e, %f' >>

(which states that the constructor for type

%t

executed in state

%f

decorated by

%a

results in the state

%f'

with behavior

%l

) then we may interpret the creation of a new

%t

object to result in behavior

%a \. %l

(where

%a

is the newly created object identifier) and state

%f'

in which the object variable x has the value

%a

. Finally, in a similar way, the method call rule states that if we assume a transition

<< S_m(e), %f^{%a} >> \apijl{%l} << %e, %f' >>

(which states that executing the statement

S_m(e)

, that is the code associated with method m and arguments e, for object

%a

in state

%f

, results in behavior

%l

and state

%f'

) then we may interpret the method call

x.m(e)

%f

as a transition to state

%f'

displaying behavior

m_{%a} \. %l

. The rules for object creation and method call already indicate that transition rules may be used to construct a complex transition from elementary steps. In other words, a transition system defines a collection of proof rules that allow us to derive (state) transitions and to characterize the behavior that may be observed. To obtain a full derivation, we need in addition to the rules for elementary statements the rules for compound statements listed in slide 10-compound.

Composition

compound

\ffrac{ $<< S_1, %f >> \apijl{ %l_1 } << %e, %f' >>$ \ifsli{\hspace{-0.5cm}}{\hspace{1cm}} $<< S_2, %f' >> \apijl{ %l_2 } << %e, %f'' >>$ }{ $<< S_1;S_2, %f >> \apijl{ %l_1 \. %l_2 } << %e, %f'' >>$ }

Conditional

$<< \! if (b) S, %f>> -> << %e, %f>>$ if $%f(b) == false$
\ffrac{ $<< S, %f >> \apijl{%l} << %e, %f' >>$ }{ $<< \! if (b) S, %f >> \apijl{%l} << %e, %f' >>$ } if \ifsli{ $%f(b)$ }{ $%f(b) == true$ }

Iteration

$<< while \; (b) S, %f>> -> << %e, %f>>$ if $%f(b) == false$
\ffrac{ $<< S, %f >> \apijl{%l} << %e, %f' >>$ }{ $<< while (b) S, %f >> \apijl{%l} << while (b) S, %f' >>$ } \ifsli{}{ if $%f(b) == true$ }

slide: Transition system -- compound statement

The composition rule states that if a statement

S_1

transforms

%f

into

%f'

with behavior

%l_1

and

S_2

transforms

%f'

into

%f''

with behavior

%l_2

then the compound statement

S_1;S_2

transforms

%f

into

%f''

with behavior

%l_1 \. %l_2

. The conditional rules state that, dependent on the value of the boolean b, the statement

if   (b)   S

has either no effect or results in a state

%f'

assuming that S transforms

%f

into

%f'

with behavior

%l

. The iteration rules state that dependent on the value of the boolean b the statement

while   (b)   S

has either no effect or results in a state

%f'

assuming that S transforms

%f

into

%f'

with behavior

%l

. In contrast to the conditional, an iteration statement is repeated when b is true, in accordance with our operational understanding of iteration.

Example

In our rules we have made a distinction between unadorned states

%f

and states

%f^{%a}

decorated with an object identifier

%a

. This reflects the distinction between the execution of a program fragment in a global context and a local context, within the confines of a particular object

%a

. Assume, for example, that we have defined a counter type ctr with a method inc that adds one to an instance variable n. In slide 10-t-example, a derivation is given of the behavior resulting from a program fragment consisting of the creation of an instance of ctr, a method call to inc and the assignment of the value of the attribute n of the counter to a variable v.

Program

$x = new ctr; x.inc(); v = x.n$

Transitions

$<< x = new ctr, %f_1 >> \apijl{ctr_1} << %e, %f_1[ x := ctr_1 ]>>$

$[1]$

$<< n = n + 1, %f_2^{%a} >> -> <<%e, %f_2[%a.n = %a.n + 1]>>$

$[2]$

$<< x.inc(), %f_2 >>$ $\apijl{inc_{%a}$ $<< %e, %f_2[%f_2(x).n := %f_2(x).n ]>>$

$[2']$

$<< v = x.n, %f_3>> -> << %e, %f_3[v := %f_3(x).n] >>$

$[3]$

Trace

$%f \apijl{%l} %f'$ with $%f = %f_1$ , $%f' = %f_3$ and $%l = ctr_1 \. inc_{ %a }$

slide: Transitions -- example

To derive the transition

%f \apijl{%l} %f'

corresponding with the program fragment

x = new   ctr; x.inc(); v = x.n

we must dissect the fragment and construct transitions for each of its (elementary) statements as shown in

[1]

[2]

and

[3]

. The second statement, the method call

x.inc()

, needs two transitions

[2]

and

[2']

, of which the first represents the execution of the body of inc in the local context of the object created in

[1]

and the second represents the effect of the method call from a global perspective. For the first statement, we have assumed that the constructor for ctr is empty and may hence be omitted. Notice that the object identifier

%a

(introduced in

[1]

) is assumed in

[2]

to effect the appropriate local changes to n. After constructing the transitions for the individual statements we may compose these transitions by applying the composition rule and, in this case, identifying

%f_2

with

%f_1[x := %a ]

and

%f_3

with

%f_2[ %a.n := %a.n + 1]

. As observable behavior we obtain

ctr_1 \. inc_{%a}

(where

ctr_1 = %a

), which represents the creation of a counter and its subsequent modification by inc.

Discussion

Transition systems, such as the one given above, were originally introduced as a means to model the behavior of CSP. They have been extensively used to model the operational semantics of programming languages, including concurrent and object-oriented languages. See, for example, [ABKR89] and [Eliens92]. In [AptO], transition systems have been used as a model to prove the soundness and completeness of correctness rules for concurrent programming constructs. Also in [AmBo93], transition systems are used to demonstrate the validity of a proof system for a parallel object-oriented programming language. The interested reader is invited to explore the sources mentioned for further study.

[] readme course preface 1 2 3 4 5 6 7 8 9 10 11 12 appendix lectures resources

eliens@cs.vu.nl

draft version 0.1 (15/7/2001)