Lab for Automated Reasoning and Analysis 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 [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).
 
sav08/normal_form_of_loop-free_programs.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice