Graphical Notation

Christoph Matheja edited this page Apr 3, 2018 · 2 revisions

This page briefly explains our graphical notation for heap configurations. An example of a heap configuration is depicted below:

A heap configuration in our graphical notation

Let us go through the elements of a heap configuration step by step.

Nodes

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.

Variables, Constants, and Markings

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

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

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].

You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.