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.

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\}}

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\}

\[ \frac{\{I\}c\{I\}}

   {\{I\}\ {\it l{}o{}o{}p}(c)\ \{I\}}

\[ \frac{\{P\}\, c_1 \{Q\} \ \ \ \{Q\}\, c_2\, \{R\}}

   {\{P\}\ c_1;c_2\ \{R\}}

\[ \frac{\{P\} c_1 \{Q\} \ \ \ \{P\} c_2 \{Q\}}

   {\{P\} c_1 [] c_2 \{Q\}}