Information Technology Reference
In-Depth Information
The introduction of error states has implication for sequential composition: all
the exception cases of program
P
are of course also the exception cases of
P
;
Q
.
Rather than change the definition of sequential composition given in [14], we
enforce these rules by means a healthiness condition. If the program
Q
is asked
to start in an exception case of its predecessor, it leaves the state unchanged
Definition 3.2
(Healthiness Condition)
(
Req
1
)
Q
=
II
Q
when the design
II
adopts the following definition
eflag
(
s
=
s
)
II
=
df
true
where
s
denotes all the state variables in the alphabet of
Q
.
Adesignis
Req
1
-healthy if it satisfies the healthiness condition
Req
1
. Define
H
1
=
df
λQ
•
(
II
eflag
Q
)
Clearly
Q
is
Req
1
healthy if and only if
Q
lies in the range of
H
1
.
The following theorem indicates
Req
1
-healthy designs are closed under conven-
tional programming combinators.
Theorem 3.1
(1)
H
1
(
P
Q
)=
H
1
(
P
)
H
1
(
Q
)
(2)
H
1
(
P
b
Q
)=
H
1
(
P
)
b
H
1
(
Q
)
(3)
H
1
(
Q
)
The basic concept of a
Req
1
-healthy design deserves a notation of its own.
Definition 3.3
(Design Matrix)
Let
D
1
=(
b
1
H
1
(
P
;
H
1
(
Q
)) =
H
1
(
P
);
R
2
) be designs of the same alphabet which
contains neither
eflag
nor
eflag
. Define
D
1
D
2
R
1
)and
D
2
=(
b
2
=
df
H
1
((
D
1
;
succ
1
)
⊕
(
D
2
;
error
1
))
where
(
v
=
v
eflag
)
succ
1
=
df
true
∧¬
(
v
=
v
eflag
)
error
1
=
df
true
∧
where
v
and
v
are the variables in the alphabet of
D
1
and
D
2
.
This definition states that
-
if the program starts in a state satisfying
b
1
, it will terminate successfully
on states satisying
R
1
.
-
if it is activated in a state satisfying
b
2
, an exception case may occur during
its execution and
R
2
will hold when the program halts.
Search WWH ::
Custom Search