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/05 10:53]
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 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 =====