\chapter{Hoare Logic}
\label{chap:hoare-logic}

\emph{Hoare logic} is due to Tony Hoare. It is also called \emph{axiomatic
semantics}. If operational semantics corresponds to an abstract interpreter,
Hoare logic corresponds to an abstract verifier. Hoare logic can be used to
specify the semantics of a programming language, but it is particularly
convenient to reason about concrete programs and prove them correct.

This chapter is inspired by Chapter~12 of \emph{Concrete
Semantics: With Isabelle\slash HOL}~\cite{nipkow-klein-2014}, whose reading
we recommend.

\section{Hoare Triples}
\label{sec:hoare-triples}

Hoare logic is a framework for deriving valid correctness formulas in a
mechanical way, using a set of axioms and proof rules. It allows us to reason
directly on the program's syntax, without concerning ourselves with the
operational semantics. The approach is mechanical in the sense that the
applicability of an axiom or a proof rule can easily be checked using a
computer or manually.

We start by introducing Hoare logic abstractly, without any connection to
Lean; later we will see how we can embed Hoare logic judgments in Lean in a
natural, useful way. The basic judgments of Hoare logic are called \emph{Hoare
triples}. They have the form \hbox{\li|{P} S {Q}|,} where \li{S} is a WHILE
statement, and \li{P} and \li{Q} are logical formulas over the state
variables. For the moment, we imagine the formulas as syntactic objects built
using the familiar connectives, without being more specific. The intended
meaning of a Hoare triple is as follows:
%
%%% TYPESETTING: repeated text
\begin{quote}
If the \emph{precondition} \li{P} is true before \li{S} is executed and the
execution terminates normally, the \emph{postcondition} \li{Q} is true at
termination.
\end{quote}

This is a \emph{partial correctness} statement: The program is correct
\emph{if} it terminates normally. For WHILE programs, the only way not to
terminate normally is to enter an infinite loop. For other programming
languages, infinite recursion and run-time errors such as division by zero
may also prevent normal termination.

Based on the intuitive interpretation of Hoare triples, all of the Hoare
triples below are valid:

\begin{center}
\li|{true} b := 4 {b = 4}| \\[\jot]
\li|{a = 2} b := 2 * a {a = 2 ∧ b = 4}| \\[\jot]
\li|{b ≥ 0} b := b + 1 {b ≥ 1}| \\[\jot]
\li|{false} skip {b = 10}| \\[\jot]
\li|{true} while i ≠ 10 do i := i + 1 {i = 10}|
\end{center}

The first three Hoare triples should be fairly intuitive.
The fourth triple is vacuously true, since the precondition \li{false} can
%%% TYPESETTING: repeated text
never be met. The part ``If the \emph{precondition} \li{P} is true'' of the
definition of Hoare triple is always false; hence the triple is true.
In a way, the triple is valid for the same reason that the assertion
\li|false → b| \li|= 10| holds for any value of \li|b|.
As for the fifth triple, there are no guarantees that control will escape the
loop (e.g., if \li{i > 10} initially), but if it does escape, then the loop's
condition must be false and hence we have the postcondition \li{i = 10}.

\section{Hoare Rules}
\label{sec:hoare-rules}

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

\begin{gather*}
\prftree[r]{\textsc{Skip}}
  {\texttt{\{{\relax P\/}\}~skip~\{{\relax P\/}\}}}
\\[2\jot]
\prftree[r]{\textsc{Asn}}
  {\texttt{\{{\relax Q}[{\relax a\/}/{\relax x\/}]\}~{\relax x\/} := {\relax a\/}~\{{\relax Q\/}\}}}
\\[2\jot]
\prftree[r]{\textsc{Seq}}
  {\texttt{\{{\relax P\/}\}~{\relax S}~\{{\relax R\/}\}}}
  {\texttt{\{{\relax R\/}\}~{\relax S\/}$'$~\{{\relax Q\/}\}}}
  {\texttt{\{{\relax P\/}\}~{\relax S}; {\relax S\/}$'$~\{{\relax Q\/}\}}}
\\[2\jot]
\prftree[r]{\textsc{If}}
  {\texttt{\{{\relax P} $\land$ {\relax b\/}\}~{\relax S}~\{{\relax Q\/}\}}}
  {\texttt{\{{\relax P} $\land$ $\lnot${\relax b\/}\}~{\relax S\/}$'$~\{{\relax Q\/}\}}}
  {\texttt{\{{\relax P\/}\}~if {\relax b\/} then {\relax S} else {\relax S\/}$'$~\{{\relax Q\/}\}}}
\\[2\jot]
\prftree[r]{\textsc{While}}
  {\texttt{\{I $\land$ {\relax b\/}\}~{\relax S}~\{I\}}}
  {\texttt{\{I\}~while {\relax b\/} do {\relax S}~\{{\relax I\/} $\land$ $\lnot${\relax b\/}\}}}
\\[2\jot]
\prftree[r]{\textsc{Conseq}}
  {\texttt{{\relax P\/}$'$ $\rightarrow$ {\relax P}}}
  {\texttt{\{{\relax P\/}\}~{\relax S}~\{{\relax Q\/}\}}}
  {\texttt{{\relax Q} $\rightarrow$ {\relax Q\/}$'$}}
  {\texttt{\{{\relax P\/}$'$\}~{\relax S}~\{{\relax Q\/}$'$\}}}
\end{gather*}

In the \textsc{Asn} rule, the
syntax $\texttt{{\relax Q}[{\relax a\/}/{\relax x\/}]}$
denotes the condition $\texttt{\relax Q}$ with $\texttt{\relax x}$
replaced by~$\texttt{\relax a}$.
Here is another way to present the \textsc{Asn} rule:
%
\[\prftree[r]{\textsc{Asn}}
  {\texttt{\{{\relax Q}[{\relax a\/}]\}~{\relax x\/} := {\relax a\/}~\{{\relax Q}[{\relax x\/}]\}}}\]
%
where $\texttt{[{\relax x\/}]}$ factors out \emph{all} occurrences of
\texttt{\relax x} in \texttt{\relax Q}.

The \textsc{Asn} rule may seem counterintuitive because it works backwards: From
the postcondition, it computes a precondition. Nevertheless, it correctly
captures the semantics of the assignment statement, as illustrated by the
following examples:
%
\begin{center}
\li|{0 = 0} x := 0 {x = 0}| \\[\jot]
\li|{0 = 0 ∧ y = 5} x := 0 {x = 0 ∧ y = 5}| \\[\jot]
\li|{x + 1 ≥ 5} x := x + 1 {x ≥ 5}|
\end{center}
%
Using elementary arithmetic, we can simplify the preconditions; for example,
\li{0 =} \li{0} is equivalent to true and \li{x + 1 ≥ 5} is equivalent to
\li{x ≥ 4}.

The \textsc{Seq} rule requires us to come up with an intermediate condition
\texttt{\relax R} that holds after executing \texttt{\relax S}
and before executing \texttt{\relax S}$'$. Here is an example of \textsc{Seq}
in action:
%
\begin{gather*}
\prftree[r]{\textsc{Seq}}
  {\prftree[r]{\textsc{Asn}}
    {\texttt{\{a = 2\} b := a \{b = 2\}}}}
  {\prftree[r]{\textsc{Asn}}
    {\texttt{\{b = 2\} c := b \{c = 2\}}}}
  {\texttt{\{a = 2\} b := a; c := b \{c = 2\}}}
\end{gather*}

In the \textsc{While} rule, the condition \li{I} is called an \emph{invariant}.
It is pre-~and postcondition of the loop itself but also of its body.
The body's precondition is strengthened with the knowledge that
\texttt{\relax b} must be true before executing the body. Moreover, the
loop's postcondition is strengthened with the knowledge that \texttt{\relax b}
must be false when the loop exits.

The \textsc{Conseq} rule is the only rule that has logical formulas among its
premises, as opposed to only Hoare triples. These conditions must be
discharged somehow---e.g., using pen and paper or a proof assistant.
\textsc{Conseq} can be used to strengthen a precondition (i.e., make it more
strict), weaken a postcondition (i.e. make it less strict), or both. An
example derivation follows:
%
\begin{gather*}
\prftree[r]{\textsc{Conseq}}
  {\texttt{x > 8 $\rightarrow$ x > 4}}
  {\prftree[r]{\textsc{Asn}\!\!\!\!\!\!\!\!\!\!} %%% TYPESETTING: hack
    {\texttt{\{x > 4\} y := x \{y > 4\}}}}
  {\texttt{y > 4 $\rightarrow$ y > 0}}
  {\texttt{\{x > 8\} y := x \{y > 0\}}}
\end{gather*}
%
Reading the tree from top to bottom, we have \emph{strengthened} the triple's
precondition from \li{x > 4} to \li{x > 8} and \emph{weakened} the
postcondition from \li{y > 4} to \li{y > 0}. We can also read the tree from
the bottom up: To prove the triple \texttt{\{x > 8\} y := x \{y > 0\}}, it
suffices to prove \texttt{\{x > 4\} y := x \{y > 4\}}, where the precondition
is \emph{weakened} and the postcondition is \emph{strengthened}.

Except for \textsc{Conseq}, the rules are syntax-driven; that is, we know which
rule to apply in each case, simply by inspecting the program at hand. If the
program is, say, an assignment, we apply the \textsc{Asn} rule---or
\textsc{Conseq}.

Some of the above rules are nonlinear---i.e., their conclusions are not of the
form \li|{P}| \li|…| \li|{Q}| for distinct variables \li{P}, \li{Q}. This makes
them inconvenient to apply. We combine some of the previous rules with
\textsc{Conseq} to derive \emph{linear} rules:
%
\begin{gather*}
\prftree[r]{\textsc{Skip}$'$}
  {\texttt{\relax P} \rightarrow \texttt{\relax Q}}
  {\texttt{\{{\relax P\/}\}~skip~\{{\relax Q\/}\}}}
\\[2\jot]
\prftree[r]{\textsc{Asn}$'$}
  {\texttt{{\relax P} $\rightarrow$ {\relax Q}[{\relax a\/}/{\relax x\/}]}}
  {\texttt{\{{\relax P\/}\}~\texttt{\relax x} := \texttt{\relax a}~\{\texttt{\relax Q\/}\}}}
\\[2\jot]
\prftree[r]{\textsc{While}$'$}
  {\texttt{\{{\relax P} $\land$ {\relax b\/}\}~{\relax S}~\{P\}}}
  {\texttt{P $\land$ $\lnot${\relax b\/} $\rightarrow$ Q}}
  {\texttt{\{P\}~while {\relax b\/} do {\relax S}~\{{\relax Q\/}\}}}
\end{gather*}
%
As an exercise, you could try to derive each of these rules from \textsc{Skip},
\textsc{Asn}, or \textsc{While} in conjunction with \textsc{Conseq}. This is not
difficult.

\section{A Semantic Approach to Hoare Logic}
\label{sec:a-semantic-approach-to-hoare-logic}

A natural way to encode Hoare logic in Lean would be to proceed roughly as we
have done for the big- and small-step semantics: Define a syntactic notion of
Hoare triple and an inductive predicate with one constructor for each of the
core Hoare rule. To represent pre- and postconditions, use predicates on
states (\li{state} \li{→ Prop}). Then we could prove \emph{soundness} with
respect to, say, the big-step semantics, meaning the following. Assume
\li|{P} S {Q}| is derivable. If \li{P s} and \li{(S,} \li{s) ⟹ t}, then
\li{Q t}. This is merely a logical rendition of the informal meaning of a
Hoare triple:
%
%%% TYPESETTING: repeated text
\begin{quote}
If the \emph{precondition} \li{P} is true before \li{S} is executed and the
execution terminates normally, the \emph{postcondition} \li{Q} is true at
termination.
\end{quote}

Instead of pursuing this approach, we propose to define Hoare triples
semantically in Lean, in terms of the big-step semantics, so that they are
correct by definition. Then we will derive the rules as lemmas, instead of
stating them as introduction rules of an inductive predicate. In conjunction
with the use of predicates to represent formulas, the approach is resolutely
semantic.

Here is the definition of a Hoare triple (for partial correctness):

\lstinputlisting[linerange=partial_hoare-q]{../lean/love09_hoare_logic_demo_master.lean}
%
Instead of writing \li{partial_hoare P S Q}, we introduce some syntactic
sugar to allow \hbox{\li|{* P *}|} \li|S| \li|{* Q *}|, which is closer to the
informal syntax \li|{P} S {Q}|.

The core Hoare rules are stated as follows:

\lstinputlisting[linerange=skip_intro-q]{../lean/love09_hoare_logic_demo_master.lean}
\lstinputlisting[linerange=assign_intro-q]{../lean/love09_hoare_logic_demo_master.lean}
\lstinputlisting[linerange=seq_intro-q]{../lean/love09_hoare_logic_demo_master.lean}
\lstinputlisting[linerange=ite_intro-q]{../lean/love09_hoare_logic_demo_master.lean}
\lstinputlisting[linerange=while_intro-q]{../lean/love09_hoare_logic_demo_master.lean}
\lstinputlisting[linerange=consequence-q]{../lean/love09_hoare_logic_demo_master.lean}

They all have proofs in terms of the big-step semantics. Some of the
triples---for example, the precondition in \li{assign_intro}---need to refer
to the state explicitly. In such case, we can use a \li{λ} to access it.
Recall that \li{P = (λs, P s)} by $\eta$-conversion. Moreover, for premise
written informally as \li{P → Q}, in Lean we must write \li{∀s, P s → Q s}.
This reflects the difference between syntactic formulas and semantic
predicates.

The syntax \li|s{n ↦ a s}| in the assignment rule denotes the state that
is identical to \li{s} at all points except \li{n} and that maps \li{n} to
\li{a s}. This state update syntax and its automation are provided by the
LoVelib library.

You might wonder, when looking at a rule such as \li{skip}, why its variable
\li{P} is not declared. To lighten notation, we have declared most of the
variables we need at the beginning of the Lean file:

\lstinputlisting[linerange=variables-q]{../lean/love09_hoare_logic_demo_master.lean}
%
Lean then adds them as implicit arguments as necessary in the definitions and
lemma statements that follow.

The formalization provide some more convenience rules, which can be derived
from the core rules:

\lstinputlisting[linerange=consequence_left-q]{../lean/love09_hoare_logic_demo_master.lean}
\lstinputlisting[linerange=consequence_right-q]{../lean/love09_hoare_logic_demo_master.lean}
\lstinputlisting[linerange=skip_intro'-q]{../lean/love09_hoare_logic_demo_master.lean}
\lstinputlisting[linerange=assign_intro'-q]{../lean/love09_hoare_logic_demo_master.lean}
\lstinputlisting[linerange=seq_intro'-q]{../lean/love09_hoare_logic_demo_master.lean}
\lstinputlisting[linerange=while_intro'-q]{../lean/love09_hoare_logic_demo_master.lean}

\section{Example: Exchanging Two Variables}
\label{sec:example-exchanging-two-variables}

Let us use the Hoare logic to verify our first program:\ a program that
exchanges the values of its variables \li{a} and \li{b}, using \li{t} for
temporary storage. The program is defined as follows:

\lstinputlisting[linerange=SWAP-q]{../lean/love09_hoare_logic_demo_master.lean}

The proof is as follows:

\lstinputlisting[linerange=SWAP_correct-q]{../lean/love09_hoare_logic_demo_master.lean}

The applications of \li{seq_intro'} and \li{assign_intro} are syntax-directed:
There are two sequential compositions and three assignments in the program and
therefore as many invocations of the corresponding rules. We end up with a very
ugly subgoal:
%
\begin{lstlisting}
∀s : state,
  s "a" = x ∧ s "b" = y →
  s{"t" ↦ s "a"}{"a" ↦ s{"t" ↦ s "a"} "b"}{"b" ↦ s{"t" ↦ s "a"}
    {"a" ↦ s{"t" ↦ s "a"} "b"} "t"} "a" = y ∧
  s{"t" ↦ s "a"}{"a" ↦ s{"t" ↦ s "a"} "b"}{"b" ↦ s{"t" ↦ s "a"}
    {"a" ↦ s{"t" ↦ s "a"} "b"} "t"} "b" = x
\end{lstlisting}
%
Fortunately, \li{simp} can simplify the subgoal dramatically, and if we enable
\emph{contextual rewriting}---an option that tell \li{simp} to use the
assumptions in the goal as rewrite rules---\li{simp} can even solve the
subgoal.

\section{Example: Adding Two Numbers}
\label{sec:example-adding-two-numbers}

Our second example computes \li{m + n}, leaving the result in \li{n},
using only these primitive operations: \li{k + 1}, \li{k - 1}, and \li{k ≠ 0}
(for arbitrary \li{k}):

\lstinputlisting[linerange=ADD-q]{../lean/love09_hoare_logic_demo_master.lean}

The proof is more involved:

\lstinputlisting[linerange=ADD_correct-q]{../lean/love09_hoare_logic_demo_master.lean}

The first step is to apply the derived \li{while} rule with a loop invariant.
Our invariant is that the sum of the program variables \li{n} and \li{m} must
be equal to the desired mathematical result \li{n₀ + m₀}, where \li{n₀} and
\li{m₀} correspond to the initial values of the program variables, as required
by the precondition.

How did we come up with this invariant? Conceptually, most invariants have the
form
%
\[\text{work already done \li{+} work remaining to be done \li{=} desired
  result}\]
%
where \li{+} in general denotes some suitable operator and not necessarily
addition. In our example, the ``work already done'' is \li{m}, the ``work
remaining to be done'' is \li{n}, and the ``desired result'' is \li{n₀ + m₀}.
When exiting the loop, we have that \li{n = 0}, so the equation simplifies to
``work already done = desired result.'' We can retrieve the desired result
from~\li{m}.

The application of \li{while_intro'} is performed using a tactic called
\li{refine}, which works like \li{exact} but lets us specify holes to be
filled later.

After applying the obvious rules on the loop body, we are left with three
subgoals. The only nontrivial subgoal is the proof that executing the body
maintains the invariant. There is some ugly arithmetic on natural numbers
necessary due to the use of the minus operator. Our proof simply performs a
case distinction to separate the zero case, where \li{- 1} has no effect
(\li{0 - 1 = 0}), and the nonzero case, where \li{- 1} has an effect. Each
case is easy to discharge using the simplifier with contextual rewriting.

\section{A Verification Condition Generator}
\label{sec:a-verification-condition-generator}

\emph{Verification condition generators} (VCGs) are programs that apply Hoare
logic rules automatically, producing \emph{verification conditions} that must
be proved by the user. The user must provide strong enough loop invariants, as
annotations in their programs. Hundreds of program verification tools are
based on these principles. Often these are based on an extension called
separation logic,%
\footnote{\url{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---i.e., rules stated to have an arbitrary \li{Q} as their postcondition;
this works well because the key rule \textsc{Asn}, for assignment, is backward.

We can use Lean's metaprogramming framework to define a simple VCG. First, we
introduce a constant called \li{while_inv} that carries an invariant \li{I} in
addition to the loop condition \li{b} and body \li{S}:

\lstinputlisting[linerange=while_inv-q]{../lean/love09_hoare_logic_demo_master.lean}

We provide two Hoare rules for the construct:\ a backward rule and a linear
rule. Both are justified in terms of the \li{while_intro'} rule we presented
earlier:

\lstinputlisting[linerange=while_inv_intro-q]{../lean/love09_hoare_logic_demo_master.lean}
%
The rules simply use the invariant annotation as their invariant. When using
the framework, we will have to be careful to provide a suitable invariant,
because there will not be a second chance to provide one.

The code of the VCG is fairly concise:

\lstinputlisting[linerange=vcg-q]{../lean/love09_hoare_logic_demo_master.lean}

The \li{is_meta} helper function determines whether a Lean term is a
metavariable (i.e., a \li{?} variable such as \li{?P}).

The VCG proper extracts the current goal---the target---and inspects it. If it
is a Hoare triple, it inspects its precondition \li{P} and statement \li{S}.
If the precondition is a metavariable, then it applies a backward rule if
there exists one (e.g., the standard assignment rule \li{assign_intro})
because this will usefully instantiate the metavariable. Otherwise, a linear
rule is used, with an arbitrary variable as its precondition, which can be
matched against the goal's precondition. For \li{while} loops, we only
consider programs that use \li{while_inv}, because we cannot guess the
invariant programmatically.

The VCG calls itself recursively on all newly emerging goals (via the \li{;}
tactic combinator) for the compound statements \li{seq}, \li{ite}, and
\li{while_inv}.

\section{Example: Adding Two Numbers, Revisited}
\label{sec:example-adding-two-numbers-revisited}

Using the verification condition generator, we can revisit the proof
of \li{ADD} presented above:

\lstinputlisting[linerange=ADD_correct₂-q]{../lean/love09_hoare_logic_demo_master.lean}

There are two main points to observe.

First, we use \li{show} to annotate the while loop with an invariant. Recall
that the \li{show} command lets us restate the goal in a computationally
equivalent way. Here, we use this facility to replace \li{while} by
\li{while_inv}, whose definition is in terms of \li{while}. The program and its
pre-~and postconditions are otherwise the same as in the lemma statement.

Second, we invoke \li{vcg} as the first proof step. This will apply all the
necessary Hoare rules and leave us with some proof goals. We first simplify
them with contextual rewriting enabled; this already takes care of two of the
three goals. For the third goal, the proof is as before.

\section{Hoare Triples for Total Correctness}
\label{sec:hoare-triples-for-total-correctness}

The focus so far in this chapter has been on partial correctness. When we
state the Hoare triple \verb|{P} S {Q}|, we claim that the final state will
satisfy \li{Q} \emph{if} the program~\li{S} terminates, but we say nothing
when \li{S} does not terminate. In particular, we can prove any
postcondition for the program \li{while true do skip}. This is admittedly too
liberal: If we are asked to provide, say, a sorting algorithm, we should not
simply give \li{while true do skip} as the answer.

\emph{Total correctness} is a stronger notion asserts that the program
terminates normally. One reason to focus on partial correctness is that it is
a necessary component of total correctness. It is also simpler, which is a
benefit in the classroom.

The Hoare triples for total correctness have the form \li{[P] S [Q]} with the
following intended meaning:
%
\begin{quote}
If the precondition \li{P} holds before \li{S} is executed, the
execution terminates normally and the postcondition \li{Q} holds in the
final state.
\end{quote}
%
For deterministic programs, the following is an equivalent formulation:
%
\begin{quote}
If the precondition \li{P} holds before \li{S} is executed, there exists a
state in which execution terminates normally and the postcondition \li{Q}
holds in that state.
\end{quote}

Here is an example Hoare triple that is valid:

\begin{center}
\li{[i ≤ 10] while i < 10 do i := i + 1 [i = 10]}
\end{center}

For the WHILE language, the distinction between partial and total correctness
only concerns \li{while} loops. The Hoare rule for \li{while} must now be
annotated by a \emph{variant} \li{V}---a natural number that decreases with
each iteration:

\begin{gather*}
\prftree[r]{\textsc{While}}
  {\texttt{[I $\land$ {\relax b\/} $\land$ V = n]~{\relax S}~[I $\land$ V < n]}}
  {\texttt{[I]~while {\relax b\/} do {\relax S}~[{\relax I\/} $\land$ $\lnot${\relax b\/}]}}
\end{gather*}
%
The variable \li{n} is a logical variable whose scope is the entire premise,
whereas \li{V} is a metavariable standing for the variant. For the example
above, we would take \li{10 - i} as the variant. A derivation tree for this
example is given on Wikipedia.%
\footnote{\url{https://en.wikipedia.org/wiki/Hoare_logic\#While_rule_for_total_correctness}}

\section{Summary of New Syntax}

\small

\subsection{Tactics}

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
\li|refine| & applies a rule that may contain holes (\li{_}) left as subgoals \\
\li{simp} \rlap{\ldots{} \verb|{ contextual := tt }|} \\
  & simplifies using assumptions in the goal as rewrite rules \\
\end{tabularx}
