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