Information Technology Reference
In-Depth Information
The definition of conditional takes the well-definedness of its Boolean test into
account
D
(
b
)
⇒
(
b
∧
beh
(
P
)
∨¬
b
∧
beh
(
Q
))
∧
beh
(
P
b
Q
)=
df
¬D
(
b
)
⇒
beh
(
halt
)
Let
{
b
i
|
1
≤
i
≤
n
}
be a set of boolean expressions, and
{
P
i
|
1
≤
i
≤
n
}
asetof
programs. The guarded choice construct
if
b
1
→
P
1
, .., b
n
→
P
n
fi
is defined by
i
(
b
i
∧D
⎛
⎞
(
b
)
∧
beh
(
P
i
))
∨
(
i
¬
⎝
⎠
beh
(
if
b
1
→
P
1
, .., b
n
→
P
n
fi
)=
df
b
i
)
∧D
(
b
)
∧
beh
(
⊥
)
∨
¬D
(
b
)
∧
beh
(
halt
)
The following theorem enables us to focus on the guarded choices with well-
defined boolean guards in the rest of this section.
Theorem 4.1
if
(
b
1
→
P
1
, ..., b
n
→
P
n
)
fi
=
if
((
b
1
D
(
b
)
false
)
→
P
1
, ..,
(
b
n
D
(
b
)
false
)
→
P
n
,
¬D
(
b
)
→
halt
)
fi
where
b
=
df
i
b
i
.
Definition 4.1
(Total assignment)
An assignment is a total one if all the variables of the program appear on the
left hand side in some standard order
x, y, .., z
:=
e, f, .., g
and all the expressions on the right hand side are well-defined.
We can transform an assignment into a total one by using guarded choice.
Theorem 4.2
x
:=
e
=
if
fi
D
(
e
)
→
x
:= (
e
D
(
e
)
x
)
,
¬D
(
e
)
→
halt
Total assignments satisfy the algebraic laws given in [14], for example
(1)
skip
=(
v
:=
v
)
(2) (
v
:=
e
;
v
:=
f
)=(
v
:=
f
(
e
))
⎛
⎞
⎛
⎞
b
1
(
v
)
→
P
1
,
b
1
(
e
)
→
(
v
:=
e
;
P
1
)
,
⎝
⎠
⎝
⎠
(3)
v
:=
e
;
if
..,
b
n
(
v
)
fi
=
if
...,
b
n
(
e
)
fi
→
P
n
→
(
v
:=
e
;
P
n
)
4.3
Scope
Let
A
,
C
and
F
be programns, and let
n
be a name. The named scope
}
n
has
n
as its name, and
A
,
C
and
F
as its forward activity, backward activity
{
A
?
C, F
Search WWH ::
Custom Search