Information Technology Reference
In-Depth Information
For any of the defined actions, the monotonicity (1) and conjunctivity (2)
properties hold:
(
p
⇒
q
)=
⇒
(
wp
(
A, p
)
⇒
wp
(
A, q
))
(1)
wp
(
A, P
)
∧
wp
(
A, Q
)
≡
wp
(
A, P
∧
Q
)
(2)
In addition, we require an action to be bounded non-deterministic. The parallel
composition of two action systems is done by joining all actions and variables.
(Some variables may be shared between the systems.) As an example, the parallel
composition
AS
1
AS
2
of two action systems
AS
1
=
[
var
X
:
T
1
=
I
1
;
do
A
1
|
A
1
m
:
u
1
...
od
]
|
AS
2
=
[
var
Z
:
T
2
=
I
2
;
do
A
1
|
A
2
n
:
u
2
...
od
]
|
yields
AS
1
2
:
AS
1
2
=
[
var
X
:
T
1
=
I
1
;
Z
:
T
2
=
I
2
;
do
A
1
|
A
1
m
...
A
1
A
2
n
...
od
:(
u
1
u
2
)
(
v
1
v
2
)
|
∪
\
∪
]
where
v
i
denotes all variables used (exported) from action system
AS
i
.
3.2 Object Orientation
We use the work of Bonsangue et al. [4] as the basis for object-oriented action
systems: in particular we share the transformation step from object-oriented
action systems to action systems. We differ in the notion of named actions and
procedures and we add the ability to prioritize objects of a particular class
with respect to objects of another class. Within our methodology, we use a very
simple form of inheritance: A class
C
2
is a valid subclass of
C
1
if and only if the
(syntactic) superposition (cf. [7]) refinement holds between the classes. Roughly
speaking this means that
C
2
may introduce additional variables and actions.
However, none of the additional actions may have any effect on the variables of
C
1
, it must be guaranteed that when only considering the new actions and the
initial state the system terminates, and the exit condition of
C
2
must imply the
exit condition of
C
1
. The subclass
C
2
may override (refine) actions of
C
1
in a
way that the guard is strengthened and values to the additional variables are
assigned.
Like most object-oriented programming languages, objects are constructed at
runtime from classes with the help of a constructor statement
o
:=
new
(
C
),
where
o
represents the instance (object) and
C
stands for some class. Similar
to [4], a class
C
is a named type and can be represented as tuple
C
=
df
(
C
n
,C
b
)
