Pushdown Systems

Pushdown systems provide a natural execution model for programs with recursion. They form a well-studied class of infinite-state systems for which many important problems like equivalence checking and model checking are decidable [4].

Definition 2 (PDS, from [7])   A pushdown system (PDS) is a tuple

$${\cal P} \;\stackrel {\Delta}{=}\; (P, \Gamma, \Delta)$$

where:

(i)

$P$ is a finite set of control locations;

(ii)

$\Gamma$ is a finite set of stack symbols;

(iii)

$\Delta \subseteq (P \times \Gamma) \times (P \times \Gamma^{\star})$ is a finite set of rewrite rules of the shape $\ensuremath{{\left< p, \gamma \right>}\xrightarrow{{\scriptsize }}{\left< q, \sigma \right>}}$.

The set $P \times \Gamma^{\star}$ are the configurations of $\cal P$. If $\ensuremath{{\left< p, \gamma \right>}\xrightarrow{{\scriptsize }}{\left< q, \sigma \right>}}$ is a rewrite rule of $\cal P$, then for each $\omega \in \Gamma^{\star}$ the configuration $\left< q, \sigma\cdot\omega \right>$ is an immediate successor of the configuration $\left< p, \gamma\cdot\omega \right>$. A run of $\cal P$ is a sequence $\rho = \left< p_0, \sigma_0 \right>\left< p_1, \sigma_1 \right>\left< p_2, \sigma_2 \right>\cdots$, such that for all $i$, $\left< p_{i+1}, \sigma_{i+1} \right>$ is an immediate successor of $\left< p_i, \sigma_i \right>$.

We now define how a set of methods $M$ induces a PDS.

Definition 3 (Induced PDS, formalising [8])   A set of methods $M$ induces a PDS

$${\cal P} \;\stackrel {\Delta}{=}\; (P, \Gamma, \Delta)$$

as follows:

(i)

$P$ consists of the single control location $p$;

(ii)

$\Gamma$ is the set $V$ of program points;

(iii)

$\Delta$ is the set $\bigcup_{m \in M} \bigcup_{v \in V_m}$   Prod$(v)$, where Prod$(v)$ is a set of rewrite rules defined as:

$$\left\{ \begin{array}{l} \left\{ \ensuremath{{\left< p, v \r... ...\ \quad\mbox{if $v : \mbox{\sf return}$} \end{array}\right.$$

The rewrite rules of the pushdown system can be interpreted as simply manipulating the calling stack of the program from which the PDS was obtained. Given a configuration $c\equiv\left< p, v\cdot\sigma \right>$ let point $(c)\;\stackrel {\Delta}{=}\; v$.