Definition:Flow Chart/Computational History

From ProofWiki
Jump to navigation Jump to search

Definition

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

Let $\struct {X, \set {f_g}, \set {f_q}}$ be an interpretation for $C$.

Let $\phi = \sequence {\tuple {b_j, x_j}}_j$ be a control path in $\tuple {C, X}$.


Let $\phi' = \sequence {\tuple {b_{j_k}, x_{j_k}}}_k$ be the subsequence of $\phi$ containing exactly those $\tuple {b_j, x_j}$ such that:

$b_j \in V_F \cup V_P$

For every $b_{j_k}$, let $O_{j_k}$ denote either:

$F_{b_{j_k}}$

or:

$P_{b_{j_k}}$

depending on whether $b_{j_k} \in V_F$ or $b_{j_k} \in V_P$.

Then the sequence $\sequence {\tuple {O_{j_k}, x_{j_k}}}_k$ is a computational history in $\tuple {C, X}$.


Sources