Information Technology Reference
In-Depth Information
and exception handler. It runs
A
first. If
A
terminates successfully, it installs
program
C
that can later be invoked by a undo command to compensate the
effect caused by the execution of
A
. Otherwise it passes the control to
F
to deal
with the exception case.
⎛
⎞
beh
(
A
);
install
(
C
);
set
(
n, C
);
exception
(
F
)
⎝
⎠
beh
(
{
A
?
C, F
}
n
)=
df
H
where
v
=
v
⎛
⎞
Cpens
=
Cpens
∧
∧
true
⎝
⎠
Cseq
=(
Cseq
·
<C>
C
=
Cseq
)
install
(
C
)=
df
true
true
v
=
v
⎛
⎞
Cseq
=
Cseq
∧
∧
true
⎝
⎠
Cpens
=
Cpens
⊕{
n
→
C
}
set
(
n, C
)=
df
true
true
exception
(
F
)=
df
((
beh
(
F
)[
false/eflag
];
beh
(
halt
))
eflag
beh
(
skip
))
where
stands for the empty text.
The unnamed scope
behaves the same as the named scope except
that it does not install a named compensation.
{
A
?
,C,F
}
⎛
⎞
beh
(
A
);
install
(
C
);
exception
(
F
)
⎝
⎠
beh
(
{
A
?
C, F
}
)=
df
H
4.4
Compensation
compensate
(
n
) activates the compensation program associated with the scope
n
.
The execition of the command
undo
switches the direction of control flow by in-
voking the compensation program stored in
Cseq
.
beh
(
undo
)=
df
beh
(
Cseq
);
beh
(
fail
)
Let
P
be a program. The notation
undo
P
represents the program which runs
P
first, then behaves like
undo
.
undo
P
=
df
beh
(
P
);
beh
(
undo
)
Search WWH ::
Custom Search