Information Technology Reference
In-Depth Information
4.3 Graph Operations
This section gives the implementation of some basic graph operations. Due to
space limitation we only present a subset of definitions below, more can be found
at
http://isg.rhul.ac.uk/morisset/sbmf/graph utl.thy
.
First, the function
swingEdge
swings an edge with the given source and label
to point to a new vertex by updating the
edgefun
of the graph. It will return
the original graph when the edge to be swung does not exist, or when the new
target is undefined.
definition
swingEdge:: vertex
⇒
label
⇒
vertex
⇒
graph
⇒
graph
where
swingEdge n x m g
≡
(
if
((getEdgeFun g) n x) =
⊥
then
g
else if
m=
⊥
then
g
else let
new EF = ((
λ
v.
λ
l. (
if
(v=n&l=x)
then
m
else
((getEdgeFun g) v l)))
in
(new EF, snd g))
We then introduce the type
path
as a list of labels, hence representing navigation
paths. For implementation optimisation reasons, the path is actually stored as
the reverse list of labels: for instance, the rCOS expression
a.b.x
is defined as the
list
[''x'', ''b'', ''a'']
.Givenapath
p
and a graph
g
, the function
getOwner
returns the vertex that the tail of the path
p
refers to in the graph. Formally,
it returns
if the path is empty, the corresponding scope node of the variable
if the path is limited to one element (using the function
getSnodeOfVar
)and
otherwise, recursively gets the owner of the tail of the path, from which it gets
the next vertex associated with the head of the tail.
consts
getOwner :: path
⇒
graph
⇒
vertex
primrec
getOwner [] g =
⊥
getOwner (x#t) g = (
if
t=[]
then
(R (getSnodeOfVar x g))
else
((getEdgeFun g) (getOwner t g) (hd t)))
Starting from the source
getOwner p g
and the label
hd p
, we can reach the
target vertex that the path
p
refers to in
g
, which is exactly the definition of the
function
getVertexPath
. This operation corresponds to the general evaluation of
path expressions in a program state.
definition
getVertexPath :: path
⇒
graph
⇒
vertex
where
getVertexPath p g
≡
(
if
p=[]
then
⊥
else
((getEdgeFun g) (getOwner p g) (hd p)))
Finally, the function
swingPath
swings the last edge of a path in the graph to
point to a new vertex. In other words, it sets a new value to a path in a state
graph, and therefore, can be used for implementing assignments in rCOS. As
defined below, it uses
getOwner
and
hd p
to find the source and the label of the
last edge respectively, and then swings the edge by using
⊥
directly.
swingEdge
When the path is empty,
swingPath
returns the original graph.
definition
swingPath :: path
⇒
vertex
⇒
graph
⇒
graph
where
swingPath p n g
≡
(
if
p=[]
then
g
else
swingEdge (getOwner p g) (hd p) n g)
This function has been proved to preserve the well-formedness,
i.e.
for any
graph
g
,anypath
p
and any non-scope node vertex
n
,if
g
is well-formed then
(swingPath p n g)
is also well-formed.
Search WWH ::
Custom Search