Differences
This shows you the differences between two versions of the page.
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 ===== |