Information Technology Reference
In-Depth Information
5
Algebraic Properties
The model we provide for compensable programs can be seen as a conservative
extension of the design model for the imperative language discussed in [14].
In particular, sequential composition, conditional and nondeterministic choice
satisfy the same laws as given in [14]. This section will investigate the algebraic
properties of the new features of compensable programs.
5.1
Composition
Sequential composition has
undo
and
halt
as its left zeroes.
(seq-1)
undo
;
Q
=
undo
(seq-2)
halt
;
Q
=
halt
5.2
Exception Handler
The exception handler
E
is defined as a binary operator of programs.
P
E
F
=
df
{
P
?
, F
}
E
distributes leftward over all programming combinators.
(
E−
1) (
P
1
P
2
)
E
F
=(
P
1
E
F
)
(
P
2
E
F
)
(
F
)
(
E−
3) If the Boolean expression
b
is well-defined, then
E−
2) (
P
1
;
P
2
)
E
F
=(
P
1
E
F
); (
P
2
E
(
P
1
b
P
2
)
E
F
=(
P
1
E
F
)
b
(
P
2
E
F
)
It is also disjunctive on its right operand.
(
E−
4)
P
E
(
F
1
F
2
)=(
P
E
F
1
)
(
P
E
F
2
)
E
has
skip
and
throw
as its right units.
(
E−
5)
(1)
P
E
skip
=
P
(2)
P
E
halt
=
P
The following laws enable us to merge the consecutive exception handlers.
(
E−
6) (
P
E
halt
)
E
F
=
P
E
F
(
E−
7) (
P
E⊥
)
E
F
=
P
E⊥
E
can be eliminated using the following laws.
(
F
=
F
;
halt
(
E−
9)
skip
E F
=
skip
(
E−
8)
halt
E
E−
10)
⊥E
F
=
⊥
(
E−
11)
undo
E
F
=
undo
Search WWH ::
Custom Search