LARA

Differences

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

Link to this comparison view

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