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