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