Program Graph
Definition
A program graph \(\texttt{PG} = (Q, \{ q_{\vartriangleright}, q_{\blacktriangleleft} \}, \texttt{Act}, \texttt{E})\) consists of the following:
- \(Q\) a finite set of Nodes.
- \(q_{\vartriangleright}, q_{\blacktriangleleft} \in Q\) two nodes called the initial node and the final node, respectively.
- \(\texttt{Act}\): a set of actions.
- \(\texttt{E} \subseteq Q \times \texttt{Act} \times Q\), a finite set of edges.
An edge \((q_\circ, \alpha, q_\bullet)\) has source node \(q_\circ\) and target node \(q_\bullet\), and it is labelled with the action 𝛼.
We shall require that the initial and final nodes are distinct and that there are no edges with source \(q_\bullet\). (Nielson and Nielson 2019, 2)
The edge labels of represent the computational "actions" that take place once the program reaches a certain state, there is no semantics behind the edges in this defiition (which is why the \(\texttt{Act}\) has a generic definition). For a semantic-based formalism look at Kripke Structures.