# 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
