# Differences

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

 sav08:summary_of_hoare_logic [2008/03/05 10:53]vkuncak sav08:summary_of_hoare_logic [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2008/03/05 10:55 vkuncak 2008/03/05 10:53 vkuncak 2008/03/04 22:31 vkuncak 2008/03/04 22:31 vkuncak 2008/03/04 22:10 vkuncak 2008/03/04 22:05 vkuncak 2008/03/04 21:40 vkuncak 2008/03/04 21:37 vkuncak 2008/03/04 21:15 vkuncak 2008/03/04 20:52 vkuncak 2008/03/04 20:49 vkuncak 2008/03/04 20:47 vkuncak 2008/03/04 20:43 vkuncak 2008/03/04 20:43 vkuncak created Next revision Previous revision 2008/03/05 10:55 vkuncak 2008/03/05 10:53 vkuncak 2008/03/04 22:31 vkuncak 2008/03/04 22:31 vkuncak 2008/03/04 22:10 vkuncak 2008/03/04 22:05 vkuncak 2008/03/04 21:40 vkuncak 2008/03/04 21:37 vkuncak 2008/03/04 21:15 vkuncak 2008/03/04 20:52 vkuncak 2008/03/04 20:49 vkuncak 2008/03/04 20:47 vkuncak 2008/03/04 20:43 vkuncak 2008/03/04 20:43 vkuncak created 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 =====