, which may be decorated by object identifiers
, as in 
.
Object identifiers are created when creating a new
instance of an object type 
.
We assume newly created object identifiers to be unique.
We assume that each object type 
has a
constructor (which is a, possibly empty,
statement that we write as 
)
and an arbitrary number of methods m.
Each method m is assumed to be defined by
some statement, which we write as 
,
for method calls of the form 
.
Also we allow an object 
of type 
to have attributes
or instance variables v that may be accessed
(read-only) as 
for an object identifier 
or 
for an object variable x (which must have
as its value).
To determine the visible behavior of a program,
we will employ labels of the form 
(to denote the creation of an object 
)
and 
(to indicate the invocation of
a method m for object 
).
We allow transitions to be labeled by sequences of
labels that we write as 
and which are concatenated
in the usual way.
We will define a transition system for a simple
language of which the syntax is defined in slide 10-syntax.
, where x is an object variable.
As elementary statements we have 
(indicating the assignment of (the value of) an expression
e to a local variable v),
(which stands for the creation of a new
object of type 
),
and 
(which calls a method m with arguments e for object x).
The object variable x is associated with an object identifier
by the state 
in which the statement in which x
occurs is executed.
As compound statements we have an empty statement
(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.
decorated by an object
identifier 
results in the empty statement
and the state 
modified by assigning
the value of e in 
(which is written as 
)
to the instance variable v of object 
.
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 
(which states that the constructor for type 
executed in state 
decorated by 
results
in the state 
with behavior 
)
then we may interpret the creation of a new 
object to result in behavior 
(where 
is the newly created object identifier)
and state 
in which the object variable x
has the value 
.
Finally, in a similar way,
the method call rule states that if we
assume
a transition 
(which states that executing
the statement 
,
that is the code associated with method m
and arguments e, for object 
in state 
,
results in behavior 
and state 
)
then we may interpret the
method call 
in 
as a transition to state 
displaying behavior
.
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.
transforms 
into 
with behavior 
and 
transforms 
into
with behavior 
then the compound statement 
transforms
into 
with behavior 
.
The conditional rules state that, dependent
on the value of the boolean b, the statement
has either no effect
or results in a state 
assuming that
S transforms 
into 
with behavior 
.
The iteration rules state that dependent
on the value of the boolean b the statement
has either no effect
or results in a state 
assuming that
S transforms 
into 
with behavior 
.
In contrast to the conditional, an iteration
statement is repeated when b is true,
in accordance with our operational
understanding of iteration.
and states 
decorated with an object identifier 
.
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 
.
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.
corresponding with the program fragment
we must dissect the fragment and construct
transitions for each of its (elementary)
statements as shown in 
, 
and 
.
The second statement, the method call 
,
needs two transitions 
and 
, of which the
first represents the execution of the body of inc
in the local context of the object created in 
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 
(introduced in 
) is assumed in 
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
with 
and
with 
.
As observable behavior we obtain 
(where 
),
which represents the creation of a counter
and its subsequent modification by inc.
|
Hush Online Technology
hush@cs.vu.nl
12/29/99 |
|
|