Definition:Flow Chart/Control Path

From ProofWiki
Jump to navigation Jump to search

Definition

Let $C = \struct {F, P, V, E}$ be a flow chart.

Let $\struct {X, \set {f_g}, \set {p_q}}$ be a interpretation for $C$.

Let $\sequence {\tuple {b_j, x_j}}_{1 \mathop \le j \mathop \le N}$ be a finite sequence in $V \times X$.


Suppose that, for every $j < N$:

$b_j b_{j + 1}$ is an arc in $E$.
If $b_j \in V_P$, then:
$x_j \in X_{b_j}$.
$b_j b_{j + 1}$ is labeled $\top$ if and only if $x_j \in p_{b_j}$.

Additionally, suppose that, for every $j < N$:

If $b_j \in V_F$, then $x_{j + 1} = \map {f_{b_j}} {x_j}$.
If $b_j \notin V_F$, then $x_{j + 1} = x_j$.


Then, $\sequence {\tuple {b_j, x_j}}_j$ is a control path in $\struct {C, X}$.


Sources