LARA

Differences

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

Link to this comparison view

sav08:hoare_logic_rule_for_loops [2008/03/04 20:33]
vkuncak
sav08:hoare_logic_rule_for_loops [2015/04/21 17:30]
Line 1: Line 1:
-====== Hoare Logic Rule for Loops ====== 
  
-The rule for simple loops is: 
- 
-\[ 
-\frac{(\models P \rightarrow I);\ \{I\}c\{I\};​\ (\models I \rightarrow Q)} 
-     ​{\{P\}\ {\it l{}o{}o{}p}\{I\}(c)\ \{Q\}} 
-\] 
- 
-We can prove that this rule is sound by induction. 
- 
-Knowing that the while loop: 
- 
-<​code>​ 
-while (F) c; 
-</​code>​ 
- 
-is equivalent with: 
- 
-<​code>​ 
-loop (assume(F); c);  
-assume(\lnot F); 
-</​code>​ 
- 
-**Question:​** What is the rule for while loops? 
-++++Hint| 
-\[ 
-\frac{(\models P \rightarrow ?);\ \{?​\}c\{?​\};​\ (\models ? \rightarrow Q)} 
-     ​{\{P\}\ {\it while}\{I\}(F)(c)\ \{Q\}} 
-\] 
-++++ 
- 
-++++Answer| 
-It follows that the rule for while loops is:  
-\[ 
-\frac{(\models P \rightarrow I);\ \{I \wedge F \}c\{I\};\ (\models (I \land \lnot F) \rightarrow Q))} 
-     ​{\{P\}\ {\it while}\{I\}(F)(c)\ \{Q\}} 
-\] 
-++++