This is an old revision of the document!
Summary of Hoare Logic
Summary of Proof Rules
We next present (one possible) summary of proof rules for Hoare logic.
Weakening and Strengthening
Strengthening precondition: \[ \frac{\models P_1 \rightarrow P_2 \ \ \ \{P_2\}c\{Q\}}
{\{P_1\}c\{Q\}}
\]
Weakening postcondition: \[ \frac{\{P\}c\{Q_1\} \ \ \ \models Q_1 \rightarrow Q_2}
{\{P\}c\{Q_2\}}
\]
Loop Free Blocks
We can directly use rules we derived in lecture04 for basic loop-free code. Either through weakest preconditions or strongest postconditions.
\[
\{wp(c,Q)\} c \{Q\}
\]
or,
\[
\{P\} c \{sp(P,c)\}
\]
For example, we have: \[
\{Q[x:=e]\}\ (x=e)\ \{Q\}
\] as well as \[
\{P\}\ assume(F)\ \{P \land F\}
\]
Loops
\[ \frac{\{I\}c\{I\}}
{\{I\}\ {\it l{}o{}o{}p}(c)\ \{I\}}
\]
Sequential Composition
\[ \frac{\{P\}\, c_1 \{Q\} \ \ \ \{Q\}\, c_2\, \{R\}}
{\{P\}\ c_1;c_2\ \{R\}}
\]
Non-Deterministic Choice
\[ \frac{\{P\} c_1 \{Q\} \ \ \ \{P\} c_2 \{Q\}}
{\{P\} c_1 [] c_2 \{Q\}}
\]
Applying Proof Rules given Invariants
Further reading
- Calculus of Computation Textbook, Chapter 5 (Program Correctness: Mechanics)
- Glynn Winskel: The Formal Semantics of Programming Languages, fourth printing, MIT Press, 1997