Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:summary_of_hoare_logic [2008/03/04 22:05] vkuncak |
sav08:summary_of_hoare_logic [2008/03/05 10:55] 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 105: | Line 106: | ||
| **Theorem:** If Hoare triple for each basic path is valid, then the Hoare triple $\{Pre\}c\{Post\}$ is valid. | **Theorem:** If Hoare triple for each basic path is valid, then the Hoare triple $\{Pre\}c\{Post\}$ is valid. | ||
| - | **Proof:** If each basic path is valid, then each path is valid, by induction and Hoare logic rule for sequential composition. Each program is of (potentially infinitely many) paths, so the property extends (Another explanation: consider any given execution and corresponding path in the control-flow graph. By induction on the length of the path we prove that all assert statements hold, up to the last one.) | + | **Proof:** If each basic path is valid, then each path is valid, by induction and Hoare logic rule for sequential composition. Each program is union of (potentially infinitely many) paths, so the property holds for the entire program. (Another explanation: consider any given execution and corresponding path in the control-flow graph. By induction on the length of the path we prove that all assert statements hold, up to the last one.) |
| The verification condition of a basic path is the formula whose validity expresses the validity of the Hoare triple for this path. | The verification condition of a basic path is the formula whose validity expresses the validity of the Hoare triple for this path. | ||
| 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)}$++ | ||
| + | |||
| + | ++Choice of annotations?|If we put annotations after if statements, we avoid exponential explosion.++ | ||
| + | |||
| ===== Further reading ===== | ===== Further reading ===== | ||
| Line 120: | Line 126: | ||
| * [[Calculus of Computation Textbook]], see Section 5.2: Partial Correctness | * [[Calculus of Computation Textbook]], see Section 5.2: Partial Correctness | ||
| * Glynn Winskel: The Formal Semantics of Programming Languages, fourth printing, MIT Press, 1997, see Section 7.4: Verification Conditions | * Glynn Winskel: The Formal Semantics of Programming Languages, fourth printing, MIT Press, 1997, see Section 7.4: Verification Conditions | ||
| - | |||
| - | |||