• English only

# 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)
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.++
+