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: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>​