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