LARA

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, see Section 5.2: Partial Correctness
  • Glynn Winskel: The Formal Semantics of Programming Languages, fourth printing, MIT Press, 1997, see Section 7.4: Verification Conditions