Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav08:summary_of_hoare_logic [2008/03/04 22:10] vkuncak |
sav08:summary_of_hoare_logic [2008/03/04 22:31] vkuncak |
||
---|---|---|---|
Line 34: | Line 34: | ||
For example, we have: | For example, we have: | ||
- | \[ | + | \[\begin{array}{l} |
- | \{Q[x:=e]\}\ (x=e)\ \{Q\} | + | \{Q[x:=e]\}\ (x=e)\ \{Q\} \\ |
- | \] | + | \ \\ |
- | as well as | + | \{\forall x.Q\}\ {\it havoc}(x)\ \{Q\} \\ |
- | \[ | + | \ \\ |
\{P\}\ assume(F)\ \{P \land F\} | \{P\}\ assume(F)\ \{P \land F\} | ||
+ | \end{array} | ||
\] | \] | ||