Information Technology Reference
In-Depth Information
many =
nx
:
0
j
!one
f
expanding !
g
=
nx
:
0
j
(
nx:coin:choc:nx:
0
)
j
!one
f
reduction
g
!
j
coin:choc:nx:
j
f
g
0
(
0
)
!one
0 is unit of !
=
coin:choc:nx:
0
j
!one
f
reduction, etc
g
def
coin
! coin:
(
choc:nx:
0
j
!one)
f
!g
coin
! choc:
nx
:
0
j
!one
f
similarly
g
choc
! nx:
0
j
!one
many
<coin;choc>
−!
many
f
local reduction
g
)many)
<coin;choc>
VM
=((
new
nx
−!
VM
This mathematical derivation is a close simulation of the execution of the
program. But does it prove that the program is correct? And what does correct-
ness mean for a programming language that has been dened only in terms of
its internal execution rather than what can be observed from outside? The usual
answer to the more general question is that a program is adequately specied
in the programming language itself by displaying the equations that it should
satisfy. For example, perhaps what we really want to prove about the vending
machine is
VM
=
coin. choc
:VM:
(In a more abstract language like CCS or CSP, such an equation would be
permitted as a recursive denition of VM). In constructing the proof of such
equations, free use may be made of all the structural laws of the calculus. But
in general the structural laws are deliberately restricted to transformations on
the static shape of a formula, and they do not give enough information about
equality of dynamically evolving behaviour. Such reasoning would require a set
of laws much larger than those postulated by the calculus. What laws should
they be? And how are they justied?
The solution to this problem is of startling originality. The user of the calculus
is allowed to extend its set of laws by any new equations that may be desired,
provided that this does not lead to a contradiction. A contradiction is dened as
the proof of an equation between processes that obviously ought to be dierent,
like a divergent process and a non-divergent one. For example, an equation
P
=
Q
leads to contradiction if you can nd some program
C
[
P
] containing
P
which
does not diverge, but when
] actually can diverge.
Finer discriminations may be imposed by dening a function
P
is replaced by
Q
,
C
[
Q
obs
(
P
), which
maps a program
P
to some simple set of observations that may be made of
it. For example,
onto the set of environments in which it
might deadlock. In each case, one might observe the set of events oered by the
environment but refused by the process. Then a contradiction is dened as a law
that equates two programs with dierent observable refusal sets. An equation
established in this way is called a
contextual equivalence
obs
(
P
)mightmap
P
Search WWH ::
Custom Search