Information Technology Reference
In-Depth Information
A named scope can be converted into an exception handler.
(
E−
12)
{
A
?
C, F
}
n
=(
A
;
{
C
}
n
)
E
F
,where
{
C
}
n
=
df
{
skip
?
C,
halt
}
n
Similar to unnamed scope we adopt the following notation for a unnamed com-
pensation program.
{
C
}
=
df
{
skip
?
C,
halt
}
No exception occurs during the execution of a total assignment, or installation
of a compensation program.
(
E−
13) (
v
:=
e
;
P
)
E
F
=(
v
:=
e
); (
P
E
F
)
(
E−
14) (
{
C
}
n
;
P
)
E
F
=
{
C
}
n
;(
P
E
F
)
(
E−
15) (
{C}
;
P
)
E F
=
{C}
;(
P E F
)
5.3
Compensation
Installation of a compensation program can be postponed.
(cpens-1)
(1)
{
C
}
n
;(
v
:=
e
)=(
v
:=
e
);
{
C
}
n
(2)
}
(cpens-2) If
b
is well-defined, then
(1)
{
C
}
;(
v
:=
e
)=(
v
:=
e
);
{
C
{
C
}
n
;(
P
b
Q
)=(
{
C
}
n
;
P
)
b
(
{
C
}
n
;
Q
)
(2)
;
Q
)
It becomes void to install a compensation program before a undo command.
(cpens-3)
(1)
{
C
}
;(
P
b
Q
)=(
{
C
}
;
P
)
b
(
{
C
}
{
C
}
n
;(
undo
P
)=
undo
(
P
;
C
)
;(
undo
P
)=
undo
(
P
;
C
)
Consecutive unnamed compensations can be merged.
(cpens-4)
{
C
}
(2)
{
C
}
;
{
D
}
=
{
D
;
C
}
6Con lu on
A theory of programming is intended to support the practice of programming by
relating each program to the specification of what it is intended to achieve. An
unifying theory is one that is applicable to a general paradigm of computing, sup-
porting the classification of many programming languages as correct instances
ofthe paradigm. This paper indicates that the UTP approach is effective in the
following aspects
Search WWH ::
Custom Search