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: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*}
 ++++ ++++
 
sav08/hoare_logic_rule_for_loops.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice