Differences

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

--- sav08:summary_of_hoare_logic [2008/03/04 21:40]
vkuncak
+++ sav08:summary_of_hoare_logic [2008/03/05 10:55]
vkuncak
@@ Line 34: / Line 34: @@
 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\}
+\end{array}
 \]
@@ Line 64: / Line 65: @@
 ===== Applying Proof Rules given Invariants =====
+Let us treat $\{P\}$ as a new kind of statement, written
+  assert(P)
+For the moment the purpose of assert is just to indicate preconditions and postconditions.  When we write
+  assert(P)
+  c1;
+  assert(Q)
+  c2;
+  assert(R)
+we expect that these Hoare triples hold:
+  {P} c1 {Q}
+  {Q} c2 {R}
+Consider control-flow graph of a program with statements assert,assume,x=e and with graph edges expressing "[]" and ";".
+We will say that the program $c$ is //sufficiently annotated// iff
+  * the first statement is assert(Pre)
+  * the last statement is assert(Post)
+  * every cycle in the control-flow graph contains at least one assert
+An assertion path is a path in its control-flow graph that starts and ends with //assert//.  Given assertion path
+  assert(P)
+  c1
+  ...
+  cK
+  assert(Q)
+we omit any assert statements in the middle, obtaining from c1,...,cK statements d1,...,dL.  We call
+\[
+   \{P\} d1\ ;\ \ldots\ ;\ dL \{Q\}
+\]
+the Hoare triple of the assertion path.
+A //basic path// is an assertion path that contains no //assert// commands other than those at the beginning and end.  Each sufficiently annotated program has finitely many basic paths.
+**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 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.
+//Simple verification conditions// for a sufficiently annotated program is the set of verification conditions for each each basic path of the program.
+One approach to verification condition generation is therefore:
+  * start with sufficiently annotated program
+  * generate 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 =====
@@ Line 69: / Line 126: @@
   * [[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