Lecture 3.2: Program Semantics — Hoare Logic

We review a second way to specify the semantics of a programming language: Hoare logic

Hoare logic

If operational semantics corresponds to an abstract interpreter, Hoare logic (also called axiomatic semantics) logic corresponds to a verifier

Hoare logic is particularly convenient to reason about programs

Hoare triples for partial correctness

The basic judgments of Hoare logic are often called Hoare triples; they have the form

{P} c {Q}

where c is a command (or statement or program), and P and Q are logical formulas over the state variables

Intended meaning:

If the precondition P holds before c is executed and the execution terminates normally, the postcondition Q holds at termination

This is a partial correctness statement: The program is correct if it terminates normally (i.e. no run-time error, no infinite loop or divergence)

Introductory examples

All of these Hoare triples are valid (with respect to the intended meaning):

• {true} b := 4 {b = 4}

• {a = 2} b := 2 * a {a = 2 ∧ b = 4}

• {b ≥ 0} b := b + 1 {b ≥ 1}

• {false} skip {b = 100}

• {true} while i ≠ 100 do i := i + 1 {i = 100}

Inference rules

The following is a complete set of rules for reasoning about WHILE programs:

———————————— Skip
{P} skip {P}


——————————————————— Asn
{Q[e/x]} x := e {Q}


{P} c {R}   {R} c' {Q}
—————————————————————— Seq
{P} c ; c' {Q}


{P ∧ b} c {Q}   {P ∧ ¬b} c' {Q}
——————————————————————————————— If
{P} if b then c else c' {Q}


{I ∧ b} c {I}
————————————————————————— While
{I} while b do c {I ∧ ¬b}


P' → P   {P} c {Q}   Q → Q'
——————————————————————————— Conseq
{P'} c {Q'}

Q[e/x] denotes Q with x replaced by e; here is another way to look at the Asn rule:

———————————————————— Asn
{Q[e]} x := e {Q[x]}

where [x] factors out all occurrences of x in Q

In the While rule, I is called an invariant

Except for Conseq, the rules are syntax-driven

Example derivations

—————————————————————— Asn   —————————————————————— Asn
{a = 2} b := a {b = 2}       {b = 2} c := b {c = 2}
——————————————————————————————————————————————————— Seq
{a = 2} b := a ; c := b {c = 2}


                 —————————————————————— Asn
x > 10 → x > 5   {x > 5} y := x {y > 5}   y > 5 → y > 0
——————————————————————————————————————————————————————— Conseq
{x > 10} y := x {y > 0}

Theoretical properties

By giving a semantic characterization of a Hoare triple in terms of an operational semantics, we can prove soundness and completeness

• Soundness: If {P} c {Q} is derivable, P s, and ⟨p, s⟩ ⟹ s', then Q s'

• Completeness: If for all s, s', P s and ⟨p, s⟩ ⟹ s' implies Q s', then {P} c {Q} is derivable

Completeness means that any WHILE program that is partially correct semantically can be proved correct using the above rules

Alternatively, we can define Hoare triples semantically in Lean; this is what we will do

We will also use predicates on states (state → Prop) to represent pre- and postconditions

The Conseq rule relies on an oracle to prove implications; if we use a proof assistant, Gödel's incompleteness theorem will (theoretically) limits which implications we can prove

Various derived rules can be proved to be correct in terms of the standard rules (or directly in terms of the semantics)

Example:

P → Q
———————————— Skip'
{P} skip {Q}

Verification condition generators

Verification condition generators (VCGs) are programs that apply Hoare logic rules automatically, producing verification conditions (VCs) that must be proved by the user

The user must usually also provide strong enough loop invariants, as an annotation in their programs

We can use Lean's metaprogramming framework to define a simple VCG

Hundreds if not thousands of program verification tools are based on these principles; often these are based on an extension called separation logic, which is sometimes called "the Hoare logic of the 21st century"

VCGs typically work backwards from the postcondition, using backward rules (rules stated to have an arbitrary Q as their postcondition); this works well because Asn is backward

Hoare triples for total correctness

Total correctness also asserts that the program terminates normally

Hoare triples have the form

[P] c [Q]

Intended meaning:

If the precondition P holds before c is executed, the execution terminates normally and the postcondition Q holds in the final state

For deterministic programs, an equivalent formulation is as follows:

If the precondition P holds before c is executed, there exists a state in which execution terminates normally and the postcondition Q holds in that state

Example:

• [i ≤ 100] while i ≠ 100 do i := i + 1 [i = 100]

In our WHILE language, this only affects while loops, which must now be annoated by a variant V (a natural number that decreases with each iteration):

[I ∧ b ∧ V = n] c [I ∧ V < n]
————————————————————————————— While
[I] while b do c [I ∧ ¬b]

Question: What is the variant in the last example?

Demo

32_lecture.lean

Newly introduced syntax

Tactics

Reference

• Concrete Semantics: With Isabelle/HOL by Tobias Nipkow and Gerwin Klein, Chapter 12

Acknowledgment

These notes are largely inspired by Concrete Semantics: With Isabelle/HOL by Tobias Nipkow and Gerwin Klein and their slides