LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
sav08:hoare_logic_rule_for_loops [2008/03/04 20:34]
vkuncak 		sav08:hoare_logic_rule_for_loops [2015/04/21 17:30] (current)
Line 3: Line 3:
 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 25: Line 25:
 **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*}
 ++++ ++++