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
Next revision Both sides next revision
sav08:hoare_logic [2009/02/25 14:34]
vkuncak
sav08:hoare_logic [2009/02/25 14:35]
vkuncak
Line 141: Line 141:
  
 We then similarly extend the notion of $sp(P,r)$ and $wp(r,Q)$ to work on formulas and commands. ​  We use the same notation and infer from the context whether we are dealing with sets and relations or formulas and commands. We then similarly extend the notion of $sp(P,r)$ and $wp(r,Q)$ to work on formulas and commands. ​  We use the same notation and infer from the context whether we are dealing with sets and relations or formulas and commands.
 +
 +
  
 ===== Composing Hoare Triples ===== ===== Composing Hoare Triples =====
Line 146: Line 148:
 \[ \[
 \frac{ \{P\} c_1 \{Q\}, \ \ \{Q\} c_2 \{R\} } \frac{ \{P\} c_1 \{Q\}, \ \ \{Q\} c_2 \{R\} }
-     { \{P\} c_1 ; c_2 \{ \} }+     { \{P\} c_1 ; c_2 \{ \} }
 \] \]
 +
 +We can prove this from 
 +  * definition of Hoare triple ​
 +  * meaning of ';'​ as $\circ$
  
 ===== Further reading ===== ===== Further reading =====
  
   * {{sav08:​backwright98refinementcalculus.pdf|Refinement Calculus Book by Back, Wright}}   * {{sav08:​backwright98refinementcalculus.pdf|Refinement Calculus Book by Back, Wright}}