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

4 Graph Representation

In [12], the state of a program is represented as a directed labeled graph. We recall
here the definition of such a graph and give its implementation in Isabelle/HOL,
together with basic operations to manipulate state graphs.

4.1 State Graph

A state graph describes the values of variables, together with a family of objects
and their relations. Due to the existence of nested local variables and method in-
vocations, we also need to describe scopes in state graphs. A scope is represented
as a node in a state graph, called scope node . Two scope nodes are adjacent iff
the scopes they represent are directly nested. They are connected by an edge la-
beled by $, the one corresponding to the inner scope as the source and the other
one as the target of the edge respectively. In particular, the top scope node with
no incoming $ edge represents the current scope, and is thus the current root of
the state graph. For instance, in Fig. 1(a), r is the root of the graph.
The outgoing edges of a scope node, except for the $ edge, represent the
variables defined in the corresponding scope. A non-scope node in a state graph
represents an object or a primitive datum, called object node and value node ,
respectively. An object node is labeled by the runtime type of the object, while
a value node is labeled by the primitive value. An outgoing edge from an object
node is labeled by a field name of the source object and refers to the target object
representing the value of this field. There is no outgoing edge from a value node.
Let A be the set of names of variables (including the special variable this

+ =

which refers to the current object) and fields, and A A∪{ $ } .Let C be the

set of classes and the set of constant values. The formal definition of a state

graph is then given as follows.

W

Definition 1 (State Graph). A state graph is a rooted, directed and labeled
graph G =

V,E,T,F,r

,where
- V = R ∪ N ∪ L is the set of nodes, where R is the set of scope nodes, N is
the set of object nodes and L is the set of value nodes,
- E ⊆ V ×A

+

× V is the set of edges,

- T : N →C is a mapping from object nodes to types,

- F : L →W is a mapping from value nodes to values,

- r ∈ R is the root of the graph and it has no incoming edges,
- starting from r ,the $ -edges, if there are any, form a path such that except
for r each node on the path has only one incoming edge.

All the nodes on the $-path are scope nodes, the top of which is the root of
the state graph. When a new scope is entered, a new node together with a $-
edge from it to the current root are pushed onto the $-path; and when a scope is
exited, the top node of the $-path is popped out, together with all edges outgoing
from it. As an illustration, Figure 1 (a) shows the state graph after the command
a.b.x :=1; var int c=2; is executed. Moreover, Figure 1 (b) shows a state graph
with recursive objects, where the types and values of nodes are ignored.