-
Notifications
You must be signed in to change notification settings - Fork 4
Graphical Notation
This page briefly explains our graphical notation for heap configurations. An example of a heap configuration is depicted below:
Let us go through the elements of a heap configuration step by step.
We depict nodes by blue circles. The number inside a node is an identifier that stays constant across program states unless a node is consumed by abstraction. This allows to track nodes while exploring a state space.
Every red box represents a variable, constant, or marking. It is labeled with the name of the variable/constant/marking in question. Moreover, each red box is attached (via a red line) to the unique node representing its value.
For example, the value of variable pos
equals the object represented by the node with identifier 2
.
Furthermore, the node with identifier 0
corresponds to the null
location, because the constant null
is attached to it.
Pointers (references) between objects are drawn as directed blue edges that are labeled with the selector corresponding to the pointer. For example, assume the node with identifier 5
represents an element of a doubly-linked list. Then its prev
pointer leads to the node with identifier 2
and its next
pointer leads to the node with identifier 4
, respectively.
Hyperedges representing abstract heap shapes instead of pointers or variables are drawn as yellow boxes that are labeled with a nonterminal.
Their sequence of attached nodes is depicted by numbered connections (corresponding to the order of the sequence) between the hyperedge and the attached nodes.
In our example from above, there is a single nonterminal hyperedge labeled with DLL
whose sequence of attached nodes is [5,4,1,0]
.