Information Technology Reference
In-Depth Information
Furthermore, we prove that a path after being swung to a vertex will actually
point to the vertex. Before stating the fact, we define a path
p
to be well-formed
w.r.t.
g
, denoted by
wfPath p g
, if, and only if, the vertex of
p
exists in
g
,andthe
owner of
p
appears exactly once as a source in the list of edges along the path,
the latest of which is exactly the property
isGoodPath p g
. For instances, in the
state graph in Figure 1 (b), the paths
v.a
,
v.a.b.c
and
v.a.b.x
satisfy
isGoodPath
,
while
v.a.b.c.a
and
v.a.b.c.a.b.x
do not. We discuss in the conclusion about the
limitations caused by this constraint.
Finally, the theorem
swingPathChangeVertex
is proved under three assump-
tions:
g
is well-formed;
p
is well-formed w.r.t.
g
;and
n
is not the undefined
vertex. In particular, with the assumption
isGoodPath
, we can prove a key fact
that the owner of the path
p
is not changed after it is swung.
theorem
swingPathChangeVertex :
wfGraph g
⇒
wfPath p g
⇒
n
=
⊥⇒
getVertexPath p (swingPath p n g) = n
We will introduce functions for implementing local variable (un-)declaration.
Adding edges representing variables in a graph is done by the function
addVarList
,
which given a function
f
of type
labelVerF
(mapping variables to their initial
values) and a graph
g
, adds edges labeled with variables
lp
in the domain of
f
to the current root of
g
and lets them point to the associated vertices
flp
.
definition
addVarList:: labelVerF
⇒
graph
⇒
graph
where
addVarList f g
≡
case
(getSnodeList g)
of
[]
⇒
g
|
a#p
⇒
((
λ
vp.
λ
lp . (
if
(vp = (R a) & (
∃
v. v
=
⊥
&flp=v))
then
(f lp)
else
((getEdgeFun g) vp lp))), snd g)
Moreover, we define a function
createSnode
which pushes a new scope node into
the scope node list of a graph. The function
Vars
then combines the operations of
creating a scope node and adding edges, and therefore implements local variable
declaration.
definition
Vars:: labelExpF
⇒
graph
⇒
graph
where
Vars f g
≡
addVarList (expToNode f (createSnode g)) (createSnode g)
where
labelExpF
maps variables to their initial expressions, and
expToNode
trans-
lates a function of type
labelExpF
to the corresponding one of type
labelVerF
,by
changing in the range the expressions to their values in the graph. Finally, we in-
troduce a function
removeSnode
which removes the top root from the scope node
list, and in consequence all edges outgoing from the scope node. It implements
local variable un-declaration.
definition
removeSnode :: graph
⇒
graph
where
removeSnode g
≡
case
(getSnodeList g)
of
[]
⇒
g
|
t#q
⇒
(
λ
v.
λ
l. (
if
(v = R t)
then
⊥
else
(getEdgeFun g) v l),
getOnodeFun g, getVnodeFun g, q)”
where the functions
getOnodeFun
and
getVnodeFun
are used to get the second and
third components of a graph respectively.
Search WWH ::
Custom Search