LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav08:summary_of_hoare_logic [2008/03/04 22:31]
vkuncak
sav08:summary_of_hoare_logic [2015/04/21 17:30] (current)
Line 8: Line 8:
  
 Strengthening precondition:​ Strengthening precondition:​
-\[+\begin{equation*}
 \frac{\models P_1 \rightarrow P_2 \ \ \ \{P_2\}c\{Q\}} \frac{\models P_1 \rightarrow P_2 \ \ \ \{P_2\}c\{Q\}}
      ​{\{P_1\}c\{Q\}}      ​{\{P_1\}c\{Q\}}
-\]+\end{equation*}
  
 Weakening postcondition:​ Weakening postcondition:​
-\[+\begin{equation*}
 \frac{\{P\}c\{Q_1\} \ \ \ \models Q_1 \rightarrow Q_2} \frac{\{P\}c\{Q_1\} \ \ \ \models Q_1 \rightarrow Q_2}
      ​{\{P\}c\{Q_2\}}      ​{\{P\}c\{Q_2\}}
-\]+\end{equation*}
  
 === Loop Free Blocks === === Loop Free Blocks ===
Line 23: Line 23:
 We can directly use rules we derived in [[lecture04]] for basic loop-free code.  Either through weakest preconditions or strongest postconditions. We can directly use rules we derived in [[lecture04]] for basic loop-free code.  Either through weakest preconditions or strongest postconditions.
  
-\[+\begin{equation*}
    ​\{wp(c,​Q)\} c \{Q\}    ​\{wp(c,​Q)\} c \{Q\}
-\]+\end{equation*}
  
 or, or,
  
-\[+\begin{equation*}
    \{P\} c \{sp(P,c)\}    \{P\} c \{sp(P,c)\}
-\]+\end{equation*}
  
 For example, we have: For example, we have:
-\[\begin{array}{l}+\begin{equation*}\begin{array}{l}
     \{Q[x:​=e]\}\ (x=e)\ \{Q\} \\      \{Q[x:​=e]\}\ (x=e)\ \{Q\} \\ 
     \ \\     \ \\
Line 41: Line 41:
      ​\{P\}\ assume(F)\ \{P \land F\}      ​\{P\}\ assume(F)\ \{P \land F\}
 \end{array} \end{array}
-\]+\end{equation*}
  
 === Loops === === Loops ===
  
-\[+\begin{equation*}
 \frac{\{I\}c\{I\}} \frac{\{I\}c\{I\}}
      ​{\{I\}\ {\it l{}o{}o{}p}(c)\ \{I\}}      ​{\{I\}\ {\it l{}o{}o{}p}(c)\ \{I\}}
-\]+\end{equation*}
  
 === Sequential Composition === === Sequential Composition ===
  
-\[+\begin{equation*}
 \frac{\{P\}\,​ c_1 \{Q\} \ \ \ \{Q\}\, c_2\, \{R\}} \frac{\{P\}\,​ c_1 \{Q\} \ \ \ \{Q\}\, c_2\, \{R\}}
      ​{\{P\}\ c_1;c_2\ \{R\}}      ​{\{P\}\ c_1;c_2\ \{R\}}
-\]+\end{equation*}
  
 === Non-Deterministic Choice === === Non-Deterministic Choice ===
  
-\[+\begin{equation*}
 \frac{\{P\} c_1 \{Q\} \ \ \ \{P\} c_2 \{Q\}} \frac{\{P\} c_1 \{Q\} \ \ \ \{P\} c_2 \{Q\}}
      ​{\{P\} c_1 [] c_2 \{Q\}}      ​{\{P\} c_1 [] c_2 \{Q\}}
-\]+\end{equation*}
  
 ===== Applying Proof Rules given Invariants ===== ===== Applying Proof Rules given Invariants =====
Line 97: Line 97:
  
 we omit any assert statements in the middle, obtaining from c1,...,cK statements d1,​...,​dL. ​ We call  we omit any assert statements in the middle, obtaining from c1,...,cK statements d1,​...,​dL. ​ We call 
-\[+\begin{equation*}
    \{P\} d1\ ;\ \ldots\ ;\ dL \{Q\}    \{P\} d1\ ;\ \ldots\ ;\ dL \{Q\}
-\]+\end{equation*}
 the Hoare triple of the assertion path.  ​ the Hoare triple of the assertion path.  ​
  
Line 106: 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 118: Line 118:
  
 In a program of size $n$, what is the ++bound on the number of basic paths?| it can be $2^{O(n)}$++ 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 123: 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
- 
-