We review a second way to specify the semantics of a programming language: 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
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 beforec
is executed and the execution terminates normally, the postconditionQ
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)
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}
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
—————————————————————— 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}
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 (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
Total correctness also asserts that the program terminates normally
Hoare triples have the form
[P] c [Q]
Intended meaning:
If the precondition
P
holds beforec
is executed, the execution terminates normally and the postconditionQ
holds in the final state
For deterministic programs, an equivalent formulation is as follows:
If the precondition
P
holds beforec
is executed, there exists a state in which execution terminates normally and the postconditionQ
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?
Name | Description |
---|---|
contradiction |
solves the goal exploiting an obvious contradiction in the hypotheses |
refine |
applies a rule that may contain holes (_ ) left as subgoals |
simp ... {contextual := tt} |
simplifies, also using assumptions in the goal as rewrite rules |
These notes are largely inspired by Concrete Semantics: With Isabelle/HOL by Tobias Nipkow and Gerwin Klein and their slides