LARA

Differences

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

Link to this comparison view

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]
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: 
-\[ 
-     (r_1 \cup r_2) \circ r_3 = (r_1 \circ r_3) \cup (r_2 \circ r_3) 
-\] 
-\[ 
-     r_3 \circ (r_1 \cup r_2) = (r_3 \circ r_1) \cup (r_3 \circ r_2) 
-\] 
-Normal form: 
-\[ 
-   ​\bigcup_{i=1}^n p_i 
-\] 
-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: 
-\[ 
-    \{ P \} r \{ Q \} 
-\] 
- 
-==== Verifying Each Path Separately ==== 
- 
-By normal form this is 
-\[ 
-    \{ P \}  \bigcup_{i=1}^n p_i \{ Q \} 
-\] 
-which is equivalent to 
-\[ 
-   ​\bigwedge_{i=1}^n (\{P\} p_i \{Q\}) 
-\] 
- 
-Note: the rule also applies to infinite union of paths (e.g. generated by loops). 
- 
-===== Three Approaches to Generate Verification Conditions ===== 
- 
-Three equivalent formulations of Hoare triple give us three approaches: 
-  - compute meaning of $c$ as a formula, then check Hoare triple (compositional approach for verification-condition generation) 
-  - compute $sp(P,r)$ as a formula, then check entailment $sp(P,r) \subseteq Q$ (forward symbolic execution) 
-  - compute $wp(Q,r)$ as a formula, then check $P \subseteq wp(Q,r)$ (backward symbolic execution)