Hoare Logic

What is Hoare Logic?

Hoare Logic is a formal logic system used for program verification. It is a system that allows us to reason formally about the correctness of a program, by ensuring the program meets specification. Ethereum uses Hoare Logic for their verification of smart contracts.

Hoare Triple

The basic structure of Hoare Logic is the Hoare triple. A Hoare triple has the form:

\begin{align} \{P\} \text{ program } \{Q\} \end{align}

With P as the pre-condition - the property that holds before the program executes.
And Q as the post-condition - the property that holds after the program finishes executing.

The basic idea being that we have a valid program whenever we begin in a state that satisfies P and the program terminates in a state that satisfies Q.

An example statement could be: \begin{align} \{x>0\}\ y:=0-x\ \{y<0\wedge y \neq x\} \end{align}