Differences

This shows you the differences between two versions of the page.

--- sav08:summary_of_hoare_logic [2008/03/04 22:31]
vkuncak
+++ sav08:summary_of_hoare_logic [2008/03/05 10:53]
vkuncak
@@ Line 106: / Line 106: @@
 **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.
@@ Line 123: / Line 123: @@
   * [[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