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:05] 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} | ||
| \] | \] | ||
| Line 115: | Line 116: | ||
| * generate simple verification conditions | * generate simple verification conditions | ||
| * prove each of the simple verification conditions | * prove each of the simple verification conditions | ||
| + | |||
| + | In a program of size $n$, what is the ++bound on the number of basic paths?| it can be $2^{O(n)}$++ | ||
| ===== Further reading ===== | ===== Further reading ===== | ||