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

If operational semantics corresponds to an idealized interpreter, \emph{Hoare
logic} corresponds to an idealized 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. It is named after its
inventor, Charles Antony Richard (Tony) Hoare. Hoare logic is also called
\emph{axiomatic semantics}.

This chapter is heavily inspired by Chapter~12 of \emph{Concrete
Semantics: With Isa\-belle\slash HOL}~\cite{nipkow-klein-2014}.

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

Hoare logic is a framework for deducing valid correctness formulas in a
mechanical way, using a set of derivation rules. It allows us to reason
directly about a program's syntax, without concerning ourselves with its
operational semantics. The approach is mechanical in the sense that the
applicability of a derivation rule can easily be checked.

We start by introducing Hoare logic abstractly, without any connection to Lean.
In a second step, we will see how we can embed Hoare logic judgments in Lean.
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 program
variables. For the moment, we imagine the formulas as syntactic objects built
using the familiar connectives and quantifiers. 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; otherwise, the program might behave
arbitrarily. 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 result in divergence or
abnormal termination.

Intuitively, all of the Hoare triples below should be valid:
%
\begin{center}
\li|{True} b := 4 {b = 4}| \\[\jot]
\li|{a = 2} b := 2 * a {a = 2 ∧ b = 4}| \\[\jot]
\li|{b ≥ 5} b := b + 1 {b ≥ 6}| \\[\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 natural.
The fourth triple is vacuously true, since the precondition \li{False} can
%%% TYPESETTING: repeated text
never be met. The part ``If the \relax{precondition} \li{P} is true'' of the
definition of Hoare triple is always false; hence the triple is true. The
triple is equivalent to the proposition \li|False → b = 10|, which holds for
any value of \li|b|. As for the fifth triple, there are no guarantees that
control will escape the loop (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}.

The following triples are bizarre but interesting:
%
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\li${False}$ & \li$S {True}$ \\[\jot]
\li${False}$ & \li$S {False}$ \\[\jot]
\li${True}$ & \li$S {True}$ \\[\jot]
\li${True}$ & \li$S {False}$
\end{tabular}
\end{center}
%
The first two triples are true of any statement \li{S} (and therefore
pointless): The precondition is never satisfied, so any postcondition holds
vacuously. The third triple is always true as well, regardless of \li{S}. The
fourth triple is true if \li{S} never terminates (e.g., \li{S :=}
\li{while True do skip}); otherwise, it is false.

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

Below we give a complete set of derivation rules for reasoning about WHILE
programs:

\ifdefined\TABLET
\vskip\abovedisplayskip
\else
\vskip\abovedisplayshortskip
\fi

\centerline{\prftree[r]{\textsc{Skip}}
  {\strut\texttt{\{{\relax P\/}\}~skip~\{{\relax P\/}\}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{Assign}}
  {\strut\texttt{\{{\relax Q}[{\relax a\/}/{\relax x\/}]\}~{\relax x\/} := {\relax a\/}~\{{\relax Q\/}\}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{Seq}}
  {\strut\texttt{\{{\relax P\/}\}~{\relax S}~\{{\relax R\/}\}}}
  {\strut\texttt{\{{\relax R\/}\}~{\relax T}~\{{\relax Q\/}\}}}
  {\strut\texttt{\{{\relax P\/}\}~{\relax S}; {\relax T}~\{{\relax Q\/}\}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{If}}
  {\strut\texttt{\{{\relax P} $\land$ {\relax B\/}\}~{\relax S}~\{{\relax Q\/}\}}}
  {\strut\texttt{\{{\relax P} $\land$ $\lnot${\relax B\/}\}~{\relax T}~\{{\relax Q\/}\}}}
  {\strut\texttt{\{{\relax P\/}\}~if {\relax B\/} then {\relax S} else {\relax T}~\{{\relax Q\/}\}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{While}}
  {\strut\texttt{\{P $\land$ {\relax B\/}\}~{\relax S}~\{P\}}}
  {\strut\texttt{\{P\}~while {\relax B\/} do {\relax S}~\{{\relax P\/} $\land$ $\lnot${\relax B\/}\}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{Conseq}}
  {\strut\texttt{{\relax P\/}$'$ $\rightarrow$ {\relax P}}}
  {\strut\texttt{\{{\relax P\/}\}~{\relax S}~\{{\relax Q\/}\}}}
  {\strut\texttt{{\relax Q} $\rightarrow$ {\relax Q\/}$'$}}
  {\strut\texttt{\{{\relax P\/}$'$\}~{\relax S}~\{{\relax Q\/}$'$\}}}}

\vskip\belowdisplayskip

\noindent
In the \textsc{Assign} rule, the
expression $\texttt{{\relax Q}[{\relax a\/}/{\relax x\/}]}$
denotes the condition $\texttt{\relax Q}$ in which all occurrences of
$\texttt{\relax x}$ are replaced by~$\texttt{\relax a}$. The rule is sometimes
presented as
%
\[\prftree[r]{\textsc{Assign}}
  {\strut\texttt{\{{\relax Q}[{\relax a\/}]\}~{\relax x\/} := {\relax a\/}~\{{\relax Q}[{\relax x\/}]\}}}\]
%
where $\texttt{[{\relax x\/}]}$ factors out the occurrences of
\texttt{\relax x} in \texttt{\relax Q}.

The \textsc{Assign} 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 below:
%
\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 computed preconditions; for
example, \li{0 = 0} is equivalent to \li{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 T}. Here is an example of \textsc{Seq}
in action:
%
\[\prftree[r]{\textsc{Seq}}
  {\prftree[r]{\textsc{Assign}}
    {\strut\texttt{\{a = 2\} b := a \{b = 2\}}}}
  {\prftree[r]{\textsc{Assign}}
    {\strut\texttt{\{b = 2\} c := b \{c = 2\}}}}
  {\strut\texttt{\{a = 2\} b := a; c := b \{c = 2\}}}\]

The \textsc{While} rule is the most intricate. The condition \li{P} is called an
\emph{invariant}. It is the pre-~and the 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. Similarly, the
loop's postcondition is strengthened with the knowledge that \texttt{\relax B}
must be false when the loop exits.

Consider an execution of a loop with
$\text{\textit n}$~iterations. Suppose that the initial state is \li{s₀} and
that the state after the \textit{i}th iteration of the loop is
\li{s}$_\text{\textit i}$. Then the following conditions will hold:
%
\begin{center}
\begin{tabular}{@{}c@{\qquad}c@{\qquad}c@{\qquad}c@{\qquad}c@{}}
\li|P s₀| & \li|P s₁ ∧ B s₁| & $\cdots$
& \li|P s|$_{\text{\textit n}-\texttt{1}}$\li| ∧ B s|$_{\text{\textit n}-\texttt{1}}$
& \li|P s|$_{\text{\textit n}}$\li| ∧ ¬ B s|$_{\text{\textit n}}$
\end{tabular}
\end{center}
%
If \text{\textit n}\li{ = 0}, we immediately have that \li|P s₀ ∧ ¬ B s₀| and
never enter the loop.

\textsc{Conseq} is the only rule that has logical formulas among its
premises, as opposed to Hoare triples. These conditions must be discharged,
whether using pen and paper or a proof assistant. \textsc{Conseq} can be used
to strengthen a precondition (i.e., make it more restrictive), weaken a
postcondition (i.e., make it less restrictive), or both. An example derivation
follows:
%
\[\tabletsmall\prftree[r]{\textsc{Conseq}}
  {\strut\texttt{x > 8 $\rightarrow$ x > 4}}
  {\prftree[r]{\textsc{Assign}\kern-3em} %%% TYPESETTING: \kern
    {\strut\texttt{\{x > 4\} y := x \{y > 4\}}}}
  {\strut\texttt{y > 4 $\rightarrow$ y > 0\,\,\,}} %%% TYPESETTING: \,'s
  {\strut\texttt{\{x > 8\} y := x \{y > 0\}}}\]
%
Reading the tree from top to bottom, we have \relax{strengthened} the triple's
precondition from \li{x > 4} to \li{x > 8} and \relax{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 \relax{weakened} and the postcondition is \relax{strengthened}.

Except for \textsc{Conseq}, the rules are \emph{syntax-driven}: We know which
rule to apply in each case, simply by inspecting the statement at hand. For an
assignment, we apply \textsc{Assign}; for a \li{while} loop, we apply
\textsc{While}; and so on.

The rules \textsc{Seq}, \textsc{If}, and \textsc{Conseq} are
\emph{bidirectional}: Their conclusions are of the form \li|{P}| \li|…|
\li|{Q}| for distinct mathematical variables \li{P}, \li{Q}. This can make
them convenient to apply. By combining the other rules with \textsc{Conseq}, we
can derive bidirectional variants:

\vskip\abovedisplayskip

\centerline{\prftree[r]{\textsc{Skip}$'$}
  {\strut\texttt{\relax P} \rightarrow \texttt{\relax Q}}
  {\strut\texttt{\{{\relax P\/}\}~skip~\{{\relax Q\/}\}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{Assign}$'$}
  {\strut\texttt{{\relax P} $\rightarrow$ {\relax Q}[{\relax a\/}/{\relax x\/}]}}
  {\strut\texttt{\{{\relax P\/}\}~\texttt{\relax x} := \texttt{\relax a}~\{\texttt{\relax Q\/}\}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{While}$'$}
  {\strut\texttt{\{{\relax P} $\land$ {\relax B\/}\}~{\relax S}~\{P\}}}
  {\strut\texttt{P $\land$ $\lnot${\relax B\/} $\rightarrow$ Q}}
  {\strut\texttt{\{P\}~while {\relax B\/} do {\relax S}~\{{\relax Q\/}\}}}}

\vskip\belowdisplayskip

\noindent
As an exercise, you could try to derive each of these rules from
\textsc{Skip}, \textsc{Assign}, or \textsc{While} in conjunction with
\textsc{Conseq}.

\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 as we
have done for the big- and small-step semantics: Define a syntactic notion of
Hoare triple and an inductive predicate, with one introduction rule for each
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 the big-step semantics, meaning the following: Whenever
\li|{P} S {Q}| is derivable, if \li{P s} and \li{(S, s) ⟹ t}, then
\li{Q t}. This is merely a logical rendition of the intuitive meaning of a
Hoare triple:
%
%%% TYPESETTING: repeated text
\begin{quote}
If the \relax{precondition} \li{P} is true before \li{S} is executed (i.e.,
\li{P s}) and the execution terminates normally (i.e., \hbox{\li{(S, s)}} \li{⟹ t}), the
\relax{postcondition} \li{Q} is true at termination (i.e., \li{Q t}).
\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
\emph{correct by definition}. Then we will derive the Hoare rules as theorems,
instead of stating them as introduction rules. In conjunction with the use of
predicates to represent formulas, this approach is resolutely semantic.

Hoare triples (for partial correctness) are defined as follows:

\lstinputlisting[linerange=PartialHoare-q]{../lean/LoVe/LoVe10_HoareLogic_DemoMaster.lean}
%
Instead of writing \li{PartialHoare P S Q}, we introduce some syntactic
sugar to allow \li|{* P *} (S) {* 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/LoVe/LoVe10_HoareLogic_DemoMaster.lean}
\betweenlistings
\lstinputlisting[linerange=assign_intro-q]{../lean/LoVe/LoVe10_HoareLogic_DemoMaster.lean}
\betweenlistings
\lstinputlisting[linerange=seq_intro-q]{../lean/LoVe/LoVe10_HoareLogic_DemoMaster.lean}
\betweenlistings
\lstinputlisting[linerange=if_intro-q]{../lean/LoVe/LoVe10_HoareLogic_DemoMaster.lean}
\betweenlistings
\lstinputlisting[linerange=while_intro-q]{../lean/LoVe/LoVe10_HoareLogic_DemoMaster.lean}
\betweenlistings
\lstinputlisting[linerange=consequence-q]{../lean/LoVe/LoVe10_HoareLogic_DemoMaster.lean}

All of the above theorems have proofs based on the big-step semantics. Some of
the triples---for example, the precondition in \li{assign_intro}---need to
refer to the state. We then use an anonymous function to
access it. Recall that \li{P} and \li{fun s ↦} \li{P s} are equal (by
\li{η}-conversion). Moreover, for a premise written informally as \li{P → Q}, in
Lean we must write \li{∀s, P s → Q s}. As in
Chapter~\ref{chap:operational-semantics}, the syntax \hbox{\li|s[x ↦ n]|} in the
assignment rule denotes the state that is identical to \li{s}
except that it maps \li{x} to \li{n}.

The following convenience rules can be derived from the core rules:

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

Using the bidirectional \li{assign_intro'}, we can derive a forward version of
the assignment rule:
%
\lstinputlisting[linerange=assign_intro_forward-q]{../lean/LoVe/LoVe10_HoareLogic_DemoMaster.lean}
%
The variable \li{n₀} stands for the value of \li{x} before the
assignment. Hence, in the postcondition, \li$s[x ↦ n₀]$ denotes the state
before the assignment. Since \li{P} is a precondition, we have
\hbox{\li$P (s[x ↦ n₀])$.} In addition, the new value of~\li{x}, given by \li{s x},
must be equal to the value of the expression \li{a} evaluated in the
old state \hbox{\li$s[x ↦ n₀]$.}

The forward rule is less convenient than the backward rule, because the
postcondition contains an existential quantifier. It is possible to state a
backward rule in a similar style, revealing a hidden symmetry:
%
\lstinputlisting[linerange=assign_intro_backward-q]{../lean/LoVe/LoVe10_HoareLogic_DemoMaster.lean}
%
Notice that this existential quantifier can be eliminated using a one-point
rule (Section~\ref{sec:forward-reasoning-about-connectives-and-quantifiers}).
We then get the familiar backward rule \li{assign_intro}, with
\li|fun s ↦| \li|P (s[x ↦ a s])| as the precondition.

\section{First Program: Exchanging Two Variables}
\label{sec:first-program-exchanging-two-variables}

Let us employ Hoare logic to verify our first program:\ a three-line 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/LoVe/LoVe10_HoareLogic_DemoMaster.lean}

The correctness statement is as follows:
%
\lstinputlisting[linerange=SWAP_correct_statement-q]{../lean/LoVe/LoVe10_HoareLogic_DemoMaster.lean}
%
The logical variables \li{a₀} and \li{b₀} ``freeze'' the initial value of the
program variables \li{a} and \li{b} so that we can refer to them in the
postcondition. After all, it would make no sense to use
\li{fun s ↦ s "a" = s "b" ∧ s "b" = s "a"} as the postcondition.

The correctness proof follows:
%
\lstinputlisting[linerange=SWAP_correct_proof-q]{../lean/LoVe/LoVe10_HoareLogic_DemoMaster.lean}
%
The applications of the sequential composition and assignment rules are guided
by the program's syntax. 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 aesthetically challenged subgoal:
%
\begin{center}
\tabletfootnotesize
\begin{tabular}{@{}l@{}}
\lic$⊢ ∀s : State,$ \\
\noindent\hbox{}\qquad\lic$s "a" = a₀ ∧ s "b" = b₀ →$ \\
\noindent\hbox{}\qquad\lic$s["t" ↦ s "a"]["a" ↦ s["t" ↦ s "a"] "b"]$ \\
\noindent\hbox{}\qquad\quad\lic$["b" ↦ s["t" ↦ s "a"]["a" ↦ s["t" ↦ s "a"] "b"] "t"] "a" = b₀ ∧$ \\
\noindent\hbox{}\qquad\lic$s["t" ↦ s "a"]["a" ↦ s["t" ↦ s "a"] "b"]$ \\
\noindent\hbox{}\qquad\quad\lic$["b" ↦ s["t" ↦ s "a"]["a" ↦ s["t" ↦ s "a"] "b"] "t"] "b" = a₀$
\end{tabular}
\end{center}
%
Fortunately, \li{simp [*] at *} can reduce the subgoal dramatically, and
\li{aesop} can even prove it fully automatically.

\section{Second Program: Adding Two Numbers}
\label{sec:second-program-adding-two-numbers}

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

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

Because of the presence of a \li{while} loop, the proof is more involved:
%
\lstinputlisting[linerange=ADD_correct-q]{../lean/LoVe/LoVe10_HoareLogic_DemoMaster.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₀ +} \hbox{\li{m₀},} where
\li{n₀} and \li{m₀} correspond to the initial values of \li{n} and \li{m}, as
required by the precondition.

How did we come up with this invariant? Even for a simple loop, finding a
suitable invariant can be challenging. The difficulty is that the invariant
must
%
\begin{itemize}
\item[1.] be true before we enter the loop;

\item[2.] remain true after each iteration of the loop if it was true before the
iteration;

\item[3.] be strong enough to imply the desired loop postcondition.
\end{itemize}
%
An invariant such as \li{True} meets requirements~1 and 2 but usually not
3. Similarly, \li{False} meets requirements 2 and 3 but not 1.
In practice, invariants tend to be of the form
%
\[\text{\emph{work done} \texttt{+} \emph{work remaining} \texttt{=} \emph{desired
  result}}\]
%
where \li{+} stands for some appropriate operator (not necessarily
addition). When we enter the loop, \emph{work done} will often be \li{0} (or
some other appropriate ``zero'' value), and the invariant becomes
%
\[\text{\emph{work remaining} \texttt{=} \emph{desired result}}\]
%
This invariant would have to be provable at the beginning of the
loop---either from the postcondition of the previous statement or from the
desired precondition of the entire program if there is no previous statement.
When we exit the loop, \emph{work remaining} should be \li{0} (or
some variant thereof), and the invariant becomes
%
\[\text{\emph{work done} \texttt{=} \emph{desired result}}\]
%
Often, \emph{work done} takes the form of a variable in which we
accumulate the result, whereas \emph{work remaining} is similar to
\emph{desired result} but depends on program variables whose values change inside
the loop and accounts for \emph{work done}.

For the \li{ADD} program's loop, the \emph{work done} is \li{m}, the \emph{work
remaining} is \li{n}, and the \emph{desired result} is \li{n₀ + m₀}.
When entering the loop, the invariant \li{m + n = n₀ + m₀} holds because then
\li{m = m₀} and \li{n = n₀}. (Unusually, the \emph{work done} is not
\li{0} for this example, because we reuse the input \li{m} as our accumulator,
as an optimization.) When exiting the loop, we have that \li{n = 0}, so the
invariant becomes \hbox{\li{m = n₀}} \li{+ m₀}. We can retrieve the result from~\li{m}.

The \li{while_intro'} theorem is used directly as a proof term. It gives rise to
three subgoals. The proofs that the invariant is implied by the desired
precondition and that it implies the desired postcondition are trivial: They
consist of a call to \li{aesop}. The only nontrivial subgoal is the condition
that executing the body maintains the invariant.

For this example, Hoare logic really helps. Reasoning directly about the
operational semantics would be inconvenient, because we would need induction to
reason about the \li{while} loop. With Hoare logic, this induction is performed
out once and for all in the proof of the \li{while_intro} rule.

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

\emph{Verification condition generators} (VCGs) are programs that apply Hoare
logic rules, producing \emph{verification conditions} that must be proved
manually. We can think of them as mechanical civil servants that take care of
the Hoare logic bureaucracy. As users, we must provide strong enough loop
invariants as annotations in our programs. Hundreds of program verification
tools are based on these principles.

VCGs typically work backwards from the postcondition, using \emph{backward}
rules---rules stated to have an arbitrary \li{Q} as their postcondition. This
works well because the central rule of Hoare logic---the assignment rule---is
backward.
%If it were not for the assignment statement, the state would never
%change, and there would be no need for Hoare logic.

We can use Lean's metaprogramming framework to define a simple VCG. First, we
introduce a constant called \li{Stmt.invWhileDo} that carries a user-supplied
invariant~\li{I} in addition to the loop condition \li{B} and the body \li{S}:

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

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

\lstinputlisting[linerange=while_inv_intro-q]{../lean/LoVe/LoVe10_HoareLogic_DemoMaster.lean}
%
The above rules simply use the invariant annotation as their invariant. When
using the framework, we will have to be careful to annotate all \li{while} loops
with suitable invariants. If we specify a wrong invariant, we will face
unprovable subgoals, indicating that we must revise the invariant.

The code of the VCG is fairly concise:

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

The VCG extracts the first goal's target and inspects it. If it is a Hoare
triple, the VCG inspects its precondition \li{P} and statement \li{S}. If the
precondition is a metavariable (e.g., \li{?P}), the VCG applies a backward rule
(via the \li{apply}\-\li{Constant} function we defined in
Section~\ref{sec:third-example-a-direct-proof-finder})
if there exists one because this will instantiate the metavariable. Otherwise, a
bidirectional rule is used, with an arbitrary variable as its precondition,
which can be matched against the target's precondition. For \li{while} loops, we
only consider programs that use \li{Stmt.invWhileDo}, because we cannot guess
the invariant programmatically.

The VCG calls itself recursively on all newly emerging subgoals for the compound
statements (via the \li{and}\-\li{ThenOnSubgoals} function we defined in
Section~\ref{sec:third-example-a-direct-proof-finder}).

\section{Second Program Revisited: Adding Two Numbers}
\label{sec:second-program-revisited-adding-two-numbers}

Using the verification condition generator, we can revisit the correctness
proof for the \li{ADD} program presented above:
%
\lstinputlisting[linerange=ADD_correct_vcg-q]{../lean/LoVe/LoVe10_HoareLogic_DemoMaster.lean}

First, we use \li{show} to annotate the \li{while} loop with an invariant. Recall that
the \li{show} command restates the goal in a computationally equivalent
way. Here, we use this facility to replace \li{Stmt.}\allowbreak\li{whileDo} by
\li{Stmt.invWhileDo}, which equals \li{Stmt.whileDo} by definition. The
program and its pre-~and postconditions are otherwise the same as in the theorem
statement.

We invoke \li{vcg} as the first proof step. This will apply all the necessary
Hoare rules and leave us with some subgoals, which are no match for \li{aesop}.

\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 \li|{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 diverging program \li{while True do skip}. This is
admittedly too liberal: If you are asked to program a sorting algorithm at an
exam, you should certainly not give \li{while True do skip} as your answer.

\emph{Total correctness} is a stronger notion that asserts, in addition to
partial correctness, that the program terminates normally. We first focused on
partial correctness because it is simpler and because it is a necessary
component of total correctness anyway.

The Hoare triples for total correctness have the form \hbox{\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, this can be expressed equivalently as follows:
%
\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 (and programs containing them). The Hoare
rule for \li{while} must now be annotated by a \emph{variant} \li{v}---a
natural number that decreases by~one or more with each iteration:
%
\[\prftree[r]{\textsc{While-Var}}
  {\strut\texttt{[P $\land$ {\relax b\/} $\land$ v = v₀]~{\relax S}~[P $\land$ v < v₀]}}
  {\strut\texttt{[P]~while {\relax b\/} do {\relax S}~[{\relax P\/} $\land$ $\lnot${\relax b\/}]}}
\]
%
Here, \li{v₀} is a logical variable that freezes \li{v}'s initial value
and whose scope is the entire premise, whereas \li{v} is a mathematical
variable (like \li{P}, \li{b}, and \li{S}). For the example above, we could
take \li{10 - i} as the variant (or \li{50 - i} or \li{1024 - i * i}).

Consider an execution \li{s₀}, \li{s₁}, $\dotsc$,
\li{s}$_{\text{\textit n}-\texttt{1}}$, \li{s}$_{\text{\textit n}}$ corresponding
to $\text{\textit n}$~loop iterations, as in Section~\ref{sec:hoare-rules}.
The following conditions will hold:

\begin{center}
\begin{tabular}{@{}c@{}c@{}c@{}c@{}c@{}c@{}c@{}c@{}c@{}}
\li|P s₀| & \hbox{\qquad} & \li|P s₁ ∧ b s₁| & \hbox{\qquad} & $\cdots$
& \hbox{\qquad}
& \li|P s|$_{\text{\textit n}-\texttt{1}}$\li| ∧ b s|$_{\text{\textit n}-\texttt{1}}$
& \hbox{\qquad}
& \li|P s|$_{\text{\textit n}}$\li| ∧ ¬ b s|$_{\text{\textit n}}$ \\[\jot]
\li|v s₀| & \li|>| & \li|v s₁| & \li|>| & $\cdots$ & \li|>| & \li|v s|$_{\text{\textit n}-\texttt{1}}$
& \li|>| & \li|v s|$_{\text{\textit n}}$ \\
\end{tabular}
\end{center}
