Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:normal_form_of_loop-free_programs [2008/03/05 10:48] vkuncak |
sav08:normal_form_of_loop-free_programs [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 11: | Line 11: | ||
Laws: | Laws: | ||
- | \[ | + | \begin{equation*} |
(r_1 \cup r_2) \circ r_3 = (r_1 \circ r_3) \cup (r_2 \circ r_3) | (r_1 \cup r_2) \circ r_3 = (r_1 \circ r_3) \cup (r_2 \circ r_3) | ||
- | \] | + | \end{equation*} |
- | \[ | + | \begin{equation*} |
r_3 \circ (r_1 \cup r_2) = (r_3 \circ r_1) \cup (r_3 \circ r_2) | r_3 \circ (r_1 \cup r_2) = (r_3 \circ r_1) \cup (r_3 \circ r_2) | ||
- | \] | + | \end{equation*} |
Normal form: | Normal form: | ||
- | \[ | + | \begin{equation*} |
\bigcup_{i=1}^n p_i | \bigcup_{i=1}^n p_i | ||
- | \] | + | \end{equation*} |
Each $p_i$ is of form $b_1 \circ \ldots \circ b_k$ for some $k$, where each $b_i$ is assignment or assume. Each $p_i$ corresponds to one of the finitely paths from beginning to end of the acyclic control-flow graph for loop-free program. | Each $p_i$ is of form $b_1 \circ \ldots \circ b_k$ for some $k$, where each $b_i$ is assignment or assume. Each $p_i$ corresponds to one of the finitely paths from beginning to end of the acyclic control-flow graph for loop-free program. | ||
Line 26: | Line 26: | ||
We want to show: | We want to show: | ||
- | \[ | + | \begin{equation*} |
\{ P \} r \{ Q \} | \{ P \} r \{ Q \} | ||
- | \] | + | \end{equation*} |
==== Verifying Each Path Separately ==== | ==== Verifying Each Path Separately ==== | ||
By normal form this is | By normal form this is | ||
- | \[ | + | \begin{equation*} |
\{ P \} \bigcup_{i=1}^n p_i \{ Q \} | \{ P \} \bigcup_{i=1}^n p_i \{ Q \} | ||
- | \] | + | \end{equation*} |
which is equivalent to | which is equivalent to | ||
- | \[ | + | \begin{equation*} |
\bigwedge_{i=1}^n (\{P\} p_i \{Q\}) | \bigwedge_{i=1}^n (\{P\} p_i \{Q\}) | ||
- | \] | + | \end{equation*} |
Note: the rule also applies to infinite union of paths (e.g. generated by loops). | Note: the rule also applies to infinite union of paths (e.g. generated by loops). |