# 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) Both sides previous revision Previous revision 2009/03/04 18:58 vkuncak 2009/03/04 18:57 vkuncak 2008/03/05 10:48 vkuncak 2008/03/04 17:32 vkuncak 2008/03/04 17:31 vkuncak 2008/03/02 22:04 vkuncak created Next revision Previous revision 2009/03/04 18:58 vkuncak 2009/03/04 18:57 vkuncak 2008/03/05 10:48 vkuncak 2008/03/04 17:32 vkuncak 2008/03/04 17:31 vkuncak 2008/03/02 22:04 vkuncak created 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); + ​ + + 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).