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