Lab for Automated Reasoning and Analysis 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 =====
 
sav08/summary_of_hoare_logic.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice