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 [2008/03/04 20:34]
vkuncak
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:
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>​
  
Line 26: Line 26:
 ++++Hint| ++++Hint|
 \[ \[
-\frac{(\models P \rightarrow ​I);\ \{?​\}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\}}
 \] \]