A Graph-Based Implementation for Mechanized Refinement Calculus of OO Programs - Formal Methods: Foundations and Applications - page 264

r

r

v

$
C

c

a

a

c

2

b

b

A

B

x

x

1

Fig. 1. (a): a state graph; (b): a state graph with recursive objects

4.2 Graph Implementation

A state graph requires the sets of scope nodes, object nodes and value nodes to
be disjoint. We therefore define the datatype vertex as the union of four disjoint
types: onode for object nodes, snode for scope nodes, vnode for value nodes, and
⊥

for the undefined vertex, the latter being introduced mainly for the definition
of graph operations.

datatype vertex = N onode | R snode | L vnode |⊥

A state graph is defined as the cartesian product of four elements:

types
edgefun = vertex ⇒ label ⇒ vertex
onodefun = onode ⇒ ctype
vnodefun = vnode ⇒ val
graph = edgefun ∗ onodefun ∗ vnodefun ∗ snode list

The first element of a graph is the function edgefun , which given a vertex a
and a label x , returns the vertex b if ( a, x, b ) is in the set of edges, ⊥ otherwise
(note that ⊥ is different from the node corresponding to null ). Such a definition
automatically ensures the determinism for edges. The second (resp. the third)
element of a graph corresponds to the function T (resp. the function F ). The
last element is a list of scope nodes, where the head of the list stands for the
current root, the second element stands for the previous one, and so on. This
representation of scope nodes allows us not to implement $-edges.
In order to ensure that there is no edge starting with the undefined vertex

⊥ ,

we introduce the following property.

definition isGoodFunction:: graph ⇒ bool where
isGoodFunction g ≡∀ x. (getEdgeFun g) ⊥ x= ⊥

where getEdgeFun g is used to get the first component of g .
Moreover, we need some properties concerning the list of scope nodes. Indeed
the snode list is well-formed (and in this case the graph satisfies isCorrectSnode ,
which we do not detail here due to lack of space) if, and only if,: (1) the scope
nodes cannot be undefined; (2) all the scope nodes are unique; (3) from each
scope node, there must exist at least one outgoing edge; (4) a scope node can
never be the target of an edge. Thus, a graph g is well-formed , denoted by
wfGraph g if, and only if, it satisfies isGoodFunction and isCorrectSnode .