• English only

# Differences

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

 sav08:hoare_logic_rule_for_loops [2008/03/04 20:33]vkuncak sav08:hoare_logic_rule_for_loops [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2008/03/04 20:34 vkuncak 2008/03/04 20:33 vkuncak 2008/03/04 20:33 vkuncak 2008/03/04 20:33 vkuncak 2008/03/04 13:01 vkuncak 2008/03/04 13:00 vkuncak 2008/03/04 12:59 vkuncak 2008/03/04 12:57 vkuncak 2008/03/04 12:54 vkuncak 2008/03/03 21:16 maria 2008/03/03 20:41 maria 2008/03/03 20:37 maria 2008/03/03 20:36 maria 2008/03/02 22:25 vkuncak created Next revision Previous revision 2008/03/04 20:34 vkuncak 2008/03/04 20:33 vkuncak 2008/03/04 20:33 vkuncak 2008/03/04 20:33 vkuncak 2008/03/04 13:01 vkuncak 2008/03/04 13:00 vkuncak 2008/03/04 12:59 vkuncak 2008/03/04 12:57 vkuncak 2008/03/04 12:54 vkuncak 2008/03/03 21:16 maria 2008/03/03 20:41 maria 2008/03/03 20:37 maria 2008/03/03 20:36 maria 2008/03/02 22:25 vkuncak created 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: ​ - is equivalent ​with: + is equivalent ​to: <​code>​ <​code>​ loop (assume(F); c); loop (assume(F); c); - assume(\lnot F); + assume(not F); ​ **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 