Hoare Logic

• Hoare Logic originated in the 1960s, but it continues to be the subject of intensive research right up to the present day. It lies at the core of a multitude of tools that are being used in academia and industry to specify and verify real software systems.

Hoare Logic

• Hoare Logic combines two beautiful ideas:
  • a natural way of writing down specifications of programs
  • a compositional proof technique for proving that programs are correct with respect to such specifications

Assertions

• We need a language that enables unambiguous specifications: we will use FOL to express assertions

A simple programming language

Here, $var$ is the name of a storage cell (variable) and $bexp$ is a quantifier-free first-order assertion.

// Oldest non-trivial algorithm known
// Assume M > 0 and N > 0 

x := M; y := N;

while x != y do
    if x<y then y := y-x
           else x := x-y

// On termination: x == y

Hoare Logic

• Hoare Logic provides axioms and inference rules for all the constructs of a programming language
• Inference rules are of the form $$\ithree{\textrm{rule name}}{\textrm{Conclusion}}{\textrm{Premise 1}}{\cdots}{\textrm{Premise n}}$$
• Rules without premises are called axioms

Axiom for skip

The command $\skipcmd$ does not change the state:

Axiom for assignment

Example

$$ \scriptsize \izero{Asgn}{\ht{\subst{(x=1)}{x}{1}}{x:=1}{x=1}} $$ which is the same as $$ \scriptsize \izero{Asgn}{\ht{1=1}{x:=1}{x=1}} $$

Consequence Rules

Note that $~~~ \scriptsize \izero{Asgn}{\ht{1=1}{x:=1}{x=1}} $

is different from $~~~ \scriptsize \izero{Asgn}{\ht{true}{x:=1}{x=1}} $

They are logically equivalent, but not syntactically equivalent!

Consequence Rules

Strengthening the precondition of a valid triple always produces another valid triple

Consequence Rules

Weakening the postcondition of a valid triple always produces another valid triple

Example: our first proof

• Putting the rules we've seen together, we can prove $$ \scriptsize {\ht{x=0}{x := x+1}{x\ge 1}} $$
• The proof is a derivation tree: $$ \scriptsize \itwo{\textrm{Conseq Pre}}{\ht{x=0}{x := x+1}{x\ge 1}} {\icond{x=0 \rightarrow x+1\ge 1}} {\izero{\textrm{Asgn}}{\ht{x+1\ge 1}{x := x+1}{x\ge 1}}} $$

Rule for Sequential Composition

• In words: if $C1$ transforms any state that satisfies $P$ into any state that satisfies $Q$, and if $C2$ transforms a state that satisfies $Q$ into any state that satisfies $R$, then $C1;C2$ transforms any state that satisfies $P$ into a state that satisfies $R$.

Example

• Show that $~~~ \scriptsize \ht{x=0}{y:=2\,;\,x:=y+1}{x=3} $
• Derivation tree:
  $ \tiny \itwo{\textrm{Seq}} {\ht{x=0}{y:=2 ; x:=y+1}{x=3}} {\itwo{\textrm{Asgn}}{\ht{x=0}{y:=2}{y+1=3}} {\icond{x=0\,\rightarrow\,2+1=3}} {\izero{\textrm{Asgn}}{\ht{2+1 = 3}{y := 2}{y+1 = 3}}}} {\izero{\textrm{Asgn}}{\ht{y+1=3}{x:=y+1}{x=3}}} $

Rule for Conditionals

• In words: if $b$ is true, the first branch is executed and we need to establish $\ht{P}{C1}{Q}$; otherwise, the second branch is executed and we need to establish $\ht{P}{C2}{Q}$

Rule for While Loops

• When the loop terminates, we know that $b$ is false
• The assertion $P$ is called an invariant

Prove that the following triple is valid

1. $\ht{x\ge 0}{\whileloop{x>0}{x:=x-1}}{x=0}$

Summary

Partial vs. Total Correctness

Consider the triple $~~\ht{P}{C}{Q}$.

• Partial correctness: if command $C$ is started in a state satisfying assertion $P$, and if $C$ terminates in some final state, then this final state will satisfy the assertion $Q$.
• Total correctness: if command $C$ is started in a state satisfying assertion $P$, then it terminates and it does so in a final state that satisfies the assertion $Q$.

Soundness

• Soundness: only valid Hoare Triples can be proved by the rules.
• To demonstrate soundness, we can use induction over the derivation trees. We have to show that:
  • The Hoare triples in the axioms are correct
  • For each inference rule, assuming that the triples in the premises are valid, we show that the triple in the conclusion is also valid.
• Soundness is proved w.r.t. the semantics of the programming language.

Completeness

• Completeness: all valid Hoare Triples can be proved by the rules.
• Completeness is relative to the logic language used.
  • For example, invariants and assertions have to be expressible in the logic.
• Soundness is proved w.r.t. the semantics of the programming language.

Decorated Programs

• Doing proofs in Hoare Logic can feel overly verbose
• Decorating programs is a way to informally write down a Hoare Logic proof
  • The idea is to insert assertions between every construct that makes the program. For example:

Decorated Programs: Skip and Assignment

Decorated Programs: Sequential Composition and While loops

Decorated Programs: Conditionals and Consequence rules

Example: A decorated program

Verify the following program by decorating it:

Invariants

• To reason about loops, we need to identify loop invariants, which might be difficult!
• For example, $\scriptsize j\ge 1$ is an invariant of the loop: $$\scriptsize i:=1;\,j:=1;\,\whileloop{i\lt n}{j:=j{+}i;\,i:=i{+}1}$$ but we cannot prove $$\scriptsize \ht{j\ge 1 \,\wedge\, i\lt n}{j:=j{+}i;\,i:=i{+}1}{j\ge 1}$$
• We need to strengthen the invariant: $\scriptsize j\ge 1 \,\wedge\, i\ge 1$