Information Technology Reference
In-Depth Information
//
(
A
1
A
2
n
...
)
od
:(
u
1
u
2
)
(
v
1
v
2
)
]
|
∪
\
∪
where
v
i
denotes all variables exported from action system
AS
i
.
Like on actions, prioritizing composition is associative on action systems. How-
ever, it does not in general distribute over parallel composition to the right when
used on action systems. This is due to local variables that would be duplicated.
3.4 Complex Data Types
Finally we add complex data types, such as maps, lists, and tuples (besides ob-
jects) to our language of OOAS. Most operators on these complex types were
taken from the set of operators defined in the Vienna Development Method
(VDM) [8,9] and include domain/range restrictions, and distributed union/in-
tersection among other standard operators. We also allow array-like access of
list elements and set operators to be working on lists.
3.5 Trace Semantics
For black-box test-case generation purposes, we are interested in the abstract
computation sequences, i.e. traces, of an action system. In [2] the computation of
an action system starting from an initial state
γ
0
is defined as a possibly infinite
sequence
t
of the form
t
=
df
γ
0
S
i
γ
1
···
with each
g.S
i
enabled in the transition's initial state.
We will use the concept of named actions to define more abstract computation
traces: we extend the name of named actions to include markers for
observable
and
controllable
actions. All methods and all unmarked actions are considered
internal
. Hence, any name
N
n
−→
of a named action is built according to the fol-
lowing grammar.
N
n
::= (
'obs'
|
'ctr'
|
''
)
''Identifier
Informally, an abstract computation sequence starting from an initial state
γ
0
is
a possibly empty or infinite sequence
t
abs
of the form
t
abs
=
df
γ
0
N
n
−→
γ
1
···
where
N
n
means the application (call) of the action body
N
b
of action
N
i
when
−→
g.N
b
holds at the transition's initial state or there is some sequence of basic
actions (including method calls)
γ
j
S
i
−→···
starting at the current state
γ
j
and
leadingtoastatewhere
g.N
b
holds.
Notice that the concept of labeled actions can already be found in [2] and
that in [10] a similar event-based view of action systems is taken.
