# 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](https://en.wikipedia.org/wiki/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`](32_lecture.lean)
## Newly introduced syntax
### Tactics
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
## Reference
* [_Concrete Semantics: With Isabelle/HOL_](http://www.concrete-semantics.org/concrete-semantics.pdf) by Tobias Nipkow and Gerwin Klein, Chapter 12
## Acknowledgment
These notes are largely inspired by [_Concrete Semantics: With Isabelle/HOL_](http://www.concrete-semantics.org/) by Tobias Nipkow and Gerwin Klein and their slides