Information Technology Reference
In-Depth Information
halt
to denote the program which always throws an exception case, and leaves
all variables unchanged.
⎛
⎝
⎞
⎠
true
true
beh
(
halt
)=
df
Identity
true
The definition of the assignment needs to take into account the possibility that
evalation of the expression is undefined..
For each expression
e
of a reasonable programming language, it is possible to
calculate a condition
(
e
), which is true in just those circumstances in which
e
can be successfully evaluated [20]. For example
D
D
(17)
=
true
D
(
true
)
=
D
(
false
)=
true
D
(
b
∨
c
)
D
(
b
)
∧D
(
c
)
=
D
(
x
)
=
true
D
(
e
+
f
)
=
D
(
e
)
∧D
(
f
)
D
(
e/f
)
=
D
(
e
)
∧D
(
f
)
∧
f
=0
D
(
e
b
f
)= (
b
⇒D
(
e
))
∧
(
¬
b
⇒D
(
f
))
if
b
is well-defined
For any expression
e
,
(
e
) is a well-defined Boolean expressuion.
Successful execution of an assignment relies on the assumption that the expres-
sion will be successfully evaluated. So we formulate our definition of assignment
D
⎛
⎝
⎞
⎠
D
(
e
)
Identity
[
v ⊕{x → e}/v
]
beh
(
x
:=
e
)=
df
¬D
(
e
)
Identity
true
Expressed in words, this definition states that
-
Either the initial values of the variables are such that evaluation of
e
fails
(
(
e
)), and the execution halts with all variables unchanged.
-
or the program terminates successfully, and the value of
x
is
e
, and the final
values of all the other variables are the same as their initial values.
¬D
4.2
Programming Combinators
The nonderterminic choice and sequential composition have exactly the same
meaning as operators on the single predicates defined in [14].
beh
(
P
;
Q
)=
df
beh
(
P
);
beh
(
Q
)
beh
(
P
Q
)=
df
beh
(
P
)
∨
beh
(
Q
)
Search WWH ::
Custom Search