• English only

# Differences

This shows you the differences between two versions of the page.

sav08:normal_form_of_loop-free_programs [2009/03/04 18:57]
vkuncak
sav08:normal_form_of_loop-free_programs [2015/04/21 17:30] (current)
Line 1: Line 1:
+====== Normal form for loop-free programs ======
+
+Example:
+<​code>​
+(if (x < 0) x=x+1 else x=x);
+(if (y < 0) y=y+x else y=y);
+</​code>​
+
+Without loops, after expressing conditionals using [] we obtain
+  c ::=  x=T | assume(F) |  c [] c  |  c ; c
+
+Laws:
+\begin{equation*}
+     (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)
+\end{equation*}
+Normal form:
+\begin{equation*}
+   ​\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.
+
+Length of normal form with sequences of if-then-else.

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).