% For a single index; for multiple indexes, see the manual
% "Instructions for preparation of papers and monographs:
% AMS-LaTeX" (instr-l.pdf in the AMS-LaTeX distribution).
\makeindex
\begin{document}
\frontmatter
\title{Formal Reasoning About Programs}
% Remove any unused author tags.
% author one information
\author{Adam Chlipala}
\address{MIT, Cambridge, MA, USA}
\email{adamc@csail.mit.edu}
\begin{abstract}
\emph{Briefly}, this book is about an approach to bringing software engineering up to speed with more traditional engineering disciplines, providing a mathematical foundation for rigorous analysis of realistic computer systems. As civil engineers apply their mathematical canon to reach high certainty that bridges will not fall down, the software engineer should apply a different canon to argue that programs behave properly. As other engineering disciplines have their computer-aided-design tools, computer science has proof assistants, IDEs for logical arguments. We will learn how to apply these tools to certify that programs behave as expected.
\emph{More specifically}: Introductions to two intertangled subjects: the Coq proof assistant, a tool for machine-checked mathematical theorem proving; and formal logical reasoning about the correctness of programs.
The classic engineering disciplines all have their standard mathematical techniques that are applied to the design of any artifact, before it is deployed, to gain confidence about its safety, suitability for some purpose, and so on.
The engineers in a discipline more or less agree on what are ``the rules'' to be followed in vetting a design.
Those rules are specified with a high degree of rigor, so that it isn't a matter of opinion whether a design is safe.
Why doesn't software engineering have a corresponding agreed-upon standard, whereby programmers convince themselves that their systems are safe, secure, and correct?
The concepts and tools may not quite be ready yet for broad adoption, but they have been under deveopment for decades.
This book introduces one particular tool and a body of ideas for how to apply it to different tasks in program proof.
As this document is in a very early draft stage, no more will be said here, in favor of jumping right into the technical material.
Eventually, there will no doubt be some sort of historical overview here, as part of a general placing-in-context of the particular approach that will come next.
There will also be plenty of scholarly citations (here and throughout the book).
In this early version, you get to take the author's word for it that we are about to learn a promising approach!
However, one overarching element of our strategy is important enough to deserve to be called out here.
We will study a variety of different approaches for formalizing what a program should do and for proving that a program does what it should.
At every step, we will pay close attention to the \emph{common foundation} that underlies everything.
For one thing, we will be proving all of our theorems with the Coq proof assistant, a powerful framework for writing and machine-checking proofs.
Coq itself is based on a relatively small set of core features, much like a well-designed programming language, and in both we build up increasingly sophisticated abstractions as libraries.
Those features can be thought of as the core of all mathematical reasoning.
We will also apply a recipe specific to program proof.
When we encounter a new challenge, to prove a new kind of property about a new kind of program, we will generally be considering four broad elements that appear in nearly all techniques.
\begin{itemize}
\item\index{encoding}\textbf{Encoding.}
Every programming language has both \index{syntax}\emph{syntax}, which defines what programs look like, and \index{semantics}\emph{semantics}, which defines how programs behave when run.
Even when these elements seem obvious intuitively, we often find that there are surprisingly subtle choices to be made in defining syntax and semantics at the highest level of rigor.
Seemingly minor decisions can have big impacts on how smoothly our proofs go.
\item\textbf{Invariants.}
Nearly every theorem about a program is stated in terms of a \index{transition system}\emph{transition system}, with some set of states and a relation for stepping from one state to the next, moving forward in time.
Nearly every program proof also works by finding an \index{invariant}\emph{invariant} of a transition system, or a property that always holds of every state reachable from some starting state.
The concept of invariant is very close to being a direct reinterpretation of mathematical induction, that glue of every serious mathematical development, known and loved by all.
\item\index{abstraction}\textbf{Abstraction.}
Often a transition system is too complex to analyze directly.
Instead, we \emph{abstract} it with another transition system that is somehow more tractable, proving that the new system preserves all relevant properties of the original.
\item\index{modularity}\textbf{Modularity.}
Similarly, when a transition system is too complex, we often break it into separate \emph{modules} and use some well-behaved composition operators to reassemble them into the whole.
Often abstraction and modularity go together, as we decompose a system both \index{horizontal decomposition}\emph{horizontally} (i.e., with modularity), splitting it into more manageable parts, and \index{vertical decomposition}\emph{vertically} (i.e., with abstraction), simplifying parts in ways that preserve key properties.
We can even alternate between strategies, breaking a system into parts, abstracting one as a simpler part, further decomposing that part into pieces, and so on.
In the course of the book, we will never quite define any of these meta-techniques in complete formality.
Instead, we'll meet many examples of each, called out by eye-catching margin notes.
Generalizing from the examples should help the reader start developing an intuition for when to use each element and for the common design patterns that apply.
The core subject matter of the book is often grouped under traditional disciplinary headers like \index{semantics}\emph{semantics}, \index{programming-languages theory}\emph{programming-languages theory}, \index{formal methods}\emph{formal methods}, and \index{verification}\emph{verification}.
Often these different traditions have their own competing terminology for shared concepts.
We'll follow one particular set of unified terminology and notation, cherry-picked from the conventions of different communities.
There really is a huge amount of commonality across everything that we'll study, so we don't want to distract by constantly translating between notations.
It is quite important to be literate in the standard notational conventions, which are almost always implemented with \index{\LaTeX{}}\LaTeX{}, and we stick entirely to that kind of notation in this book.
However, we follow another, much less usual convention: while we give theorem and lemma statements, we rarely give their proofs.
The reason is that the author and many other researchers today feel that proofs on paper have outlived their usefulness.
Instead, the proofs are all found in the parallel world of the accompanying Coq source code.
That is, each chapter of this book has a corresponding Coq source file, distributed with the general book source code.
The Coq sources are heavily commented and may even, in many cases, be feasible to read without also reading the book chapters.
More importantly, the Coq sources aren't just meant to be \emph{read}.
They are meant to be \emph{executed}.
We suggest stepping through them interactively, seeing intermediate states of proofs as appropriate.
The book proper can be read without the Coq sources, to learn the standard background material of program proof; and the Coq sources can be read without the book proper, to learn a particular concrete realization of those ideas.
The definition of a program starts with the definition of a programming language, and the definition of a programming language starts with its \emph{syntax}\index{syntax}, which covers which sorts of phrases are basically well-formed.
In the next chapter, we turn to \emph{semantics}\index{semantics}, which, in the course of saying what programs \emph{mean}, may impose further validity conditions.
Turning to examples, let's start with \emph{concrete syntax}\index{concrete syntax}, which decrees which sequences of characters are acceptable.
For a simple language of arithmetic expressions, we might accept the following strings as valid.
$$\begin{array}{l}
3 \\
x \\
3 + x \\
y * (3 + x)
\end{array}$$
Plenty of other strings might be invalid, like these.
$$\begin{array}{l}
1 + + \; 2 \\
x \; y \; z
\end{array}$$
Rather than appeal to our intuition about grade-school arithmetic, we prefer to formalize concrete syntax with a \emph{grammar}\index{grammar}, following a style known as \emph{Backus-Naur Form (BNF)}\index{Backus-Naur Form}\index{BNF}.
We have a set of \emph{nonterminals}\index{nonterminal} (e.g., $e$ below), standing for sets of allowable strings.
Some are defined by appeal to existing sets, as below, when we define constants $n$ in terms of the well-known set $\mathbb N$\index{N@$\mathbb N$} of natural numbers\index{natural numbers} (nonnegative integers).
\textrm{Expressions}& e &::=& n \mid x \mid e + e \mid e \times e
\end{array}$$
To interpret the grammar in plain English: we assume sets of constants and variables, based on well-known sets of natural numbers and strings, respectively.
We then define expressions to include constants, variables, addition, and multiplication.
Crucially, the last two cases are specified \emph{recursively}: we show how to build bigger expressions out of smaller ones.
Incidentally, we're already seeing how many different formal notations creep into the discussion of formal program proofs.
All of this content is typeset in \LaTeX{}\index{\LaTeX{}}, and it may be helpful to consult the book sources, to see how it's all done.
Throughout the subject, one of our most crucial tools will be \emph{inductive definitions}\index{inductive definition}, explaining how to build up bigger sets from smaller ones.
The recursive nature of the grammar above is implicitly giving an inductive definition.
A more general notation for inductive definitions provides a series of \emph{inference rules}\index{inference rules} that define a set.
Formally, the set is defined to be \emph{the smallest one that satisfies all the rules}.
Each rule has \emph{premises}\index{premise} and a \emph{conclusion}\index{conclusion}.
We illustrate with four rules that together are equivalent to the BNF grammar above, for defining a set $\mathsf{Exp}$ of expressions.
The general reading of an inference rule is: \textbf{if} all the facts above the horizontal line are true, \textbf{then} the fact below the line is true, too.
The rule implicitly needs to hold for \emph{all} values of the \emph{metavariables}\index{metavariable} (like $n$ and $e_1$) that appear within it; we can model them more explicitly with a sort of top-level universal quantification.
Newcomers to semantics often react negatively to seeing this style of definition, but very quickly it becomes apparent as a remarkably compact notation for expressing many concepts.
Think of it as a domain-specific programming language for mathematical definitions, an analogy that becomes quite concrete in the associated Coq code!
\section{Abstract Syntax}
After that brief interlude with concrete syntax, we now drop all formal treatment of it, for the rest of the book!
Instead, we concern ourselves with \emph{abstract syntax}\index{abstract syntax}, the real heart of language definitions.
Now programs are \emph{abstract syntax trees}\index{abstract syntax tree} (\emph{ASTs}\index{AST}), corresponding to inductive type definitions in Coq or algebraic datatype\index{algebraic datatype} definitions in Haskell\index{Haskell}.
Such types can be defined by enumerating their \emph{constructor}\index{constructor} functions with types.
Actually, semanticists get tired of writing such verbose descriptions, so proofs on paper tend to use exactly the sort of notation that we associated with concrete syntax.
The trick is mental desugaring of the concrete-syntax notation into abstract syntax!
We will generally not dwell on the particularities of that process.
Instead, we repeatedly illustrate it by example, using Coq code that starts with abstract syntax, accompanied by \LaTeX{}-based ``code'' in this book that applies concrete syntax freely.
Abstract syntax is handy for writing \emph{recursive definitions}\index{recursive definition} of functions.
Here is one in the clausal\index{clausal function definition} style of Haskell\index{Haskell}.
It is important that we include \emph{one clause per constructor of the inductive type}.
Otherwise, the function would not be \emph{total}\index{total function}.
We also need to be careful to ensure \emph{termination}\index{termination of recursive definitions}, by making recursive calls only on the arguments of the constructors.
This termination criterion, adopted by Coq, is called \emph{primitive recursion}\index{primitive recursion}.
Let's continue to exercise our creative license and write $\depth{e}$ for the \emph{depth} of $e$, that is, the length of the longest downward path from the syntax-tree root to any leaf.
The main reason to prefer abstract syntax is that, while strings of text \emph{seem} natural and simple to our human brains, they are really a lot of trouble to treat in complete formality.
Inductive trees are much nicer to manipulate.
Considering the name, it's probably not surprising that the main thing we want to do on them is \emph{induction}\index{induction}, an activity most familiar in the form of \emph{mathematical induction}\index{mathematical induction} over the natural numbers.
In this book, we will not dwell on many proofs about natural numbers, instead presenting the more general and powerful idea of \emph{structural induction}\index{structural induction} that subsumes mathematical induction in a formal sense, based on viewing the natural numbers as one simple inductively defined set.
There is a general recipe to go from an inductive definition to its associated induction principle.
When we define set $S$ inductively, we gain an induction principle for proving that some predicate $P$ holds for all elements of $S$.
To make this conclusion, we must discharge one proof obligation per rule of the inductive definition.
Recall our last rule-based definition above, for the abstract syntax of $\mathsf{Exp}$.
To derive an $\mathsf{Exp}$ structural induction principle, we produce a new set of rules, cloning each rule with two key modifications:
\begin{enumerate}
\item Replace each conclusion, of the form $E \in S$, with a conclusion $P(E)$. That is, the obligations involve \emph{showing} that $P$ holds of certain terms.
\item For each premise $E \in S$, add a companion premise $P(E)$. That is, the obligation allows \emph{assuming} that $P$ holds of certain terms. Each such assumption is called an \emph{inductive hypothesis}\index{inductive hypothesis} (\emph{IH}\index{IH}).
\end{enumerate}
That mechanical procedure derives the following four proof obligations, associated with an inductive proof that $\forall x \in\mathsf{X}. \; P(x)$.
$$\infer{P(\mathsf{Const}(n))}{
n \in\mathbb N
}
\quad\infer{P(\mathsf{Var}(x))}{
x \in\mathsf{Strings}
}$$
$$\quad\infer{P(\mathsf{Plus}(e_1, e_2))}{
e_1 \in\mathsf{Exp}
& P(e_1)
& e_2 \in\mathsf{Exp}
& P(e_2)
}
\quad\infer{P(\mathsf{Times}(e_1, e_2))}{
e_1 \in\mathsf{Exp}
& P(e_1)
& e_2 \in\mathsf{Exp}
& P(e_2)
}$$
In other words, to establish $\forall x \in\mathsf{X}. \; P(x)$, we need to prove that each of these inference rules is valid.
To see induction in action, we prove a theorem giving a sanity check on our two recursive definitions from earlier: depth can never exceed size.
\begin{theorem}
For all $e \in\mathsf{Exp}$, $\depth{e}\leq\size{e}$.
\end{theorem}
\begin{proof}
By induction on the structure of $e$.
\end{proof}
That sort of minimalist proof often surprises and frustrates newcomers.
Our position here is that proof checking is an activity fit for machines, not people, so we will leave out gory details, which are to be found in the accompanying Coq code, for this theorem and many others associated with this chapter.
Actually, even published proofs on paper tend to use ``proofs'' as brief as the one above, relying on the reader's experience to ``fill in the blanks''!
Unsurprisingly, fairly often there are logical errors in such arguments, leading to acceptance of bogus theorems.
For that reason, we stick to machine-checked proofs here, using the book chapters to introduce concepts, reasoning principles, and statements of key theorems and lemmas.
We do, however, need to get all the proof details filled in somehow.
One of the most convenient cases is when a proof goal fits into some \emph{decidable theory}\index{decidable theory}.
We follow the sense from computability theory\index{computability theory}, where we consider some \emph{decision problem}\index{decision problem}, as a (usually infinite) set $F$ of formulas and some subset $T \subseteq F$ of \emph{true} formulas, possibly considering only those provable using some limited set of inference rules.
The decision problem is \emph{decidable} if and only if there exists some always-terminating program that, when passed some $f \in F$ as input, returns ``true'' if and only if $f \in T$.
Decidability of theories is handy because, whenever our goal belongs to the $F$ set of a decidable theory, we can discharge the goal automatically by running the deciding program that must exist.
One common decidable theory is \emph{linear arithmetic}\index{linear arithmetic}, whose $F$ set is generated by the following grammar as $\phi$.
$$\begin{array}{rrcl}
\textrm{Constants}& n &\in&\mathbb Z \\
\textrm{Variables}& x &\in&\mathsf{Strings}\\
\textrm{Terms}& e &::=& x \mid n \mid e + e \mid e - e \\
\textrm{Propositions}&\phi&::=& e = e \mid e < e \mid\neg\phi\mid\phi\land\phi
\end{array}$$
The arithmetic terms used here are \emph{linear} in the same sense as \emph{linear algebra}\index{linear algebra}: we never multiply together two terms containing variables.
Actually, multiplication is prohibited outright, but we allow multiplication by a constant as an abbreviation (logically speaking) for repeated addition.
Propositions are formed out of equality and less-than tests on terms, and we also have the Boolean negation (``not'') operator $\neg$ and conjunction (``and'') operator $\land$.
This set of propositional\index{propositional logic} operators is enough to encode the other usual inequality and propositional operators, so we allow them, too, as convenient shorthands.
Using decidable theories in a proof assistant like Coq, it is important to understand how a theory may apply to formulas that don't actually satisfy its grammar literally.
As one more example of a decidable theory, consider the algebraic structure of \emph{semirings}\index{semirings}, which may profitably be remembered as ``types that act like natural numbers.''
A semiring is any set containing two elements notated 0 and 1, closed under two binary operators notated $+$ and $\times$.
The notations are suggestive, but in fact we have free reign in choosing the set, elements, and operators, so long as the following axioms\footnote{The equations are taken almost literally from \url{https://en.wikipedia.org/wiki/Semiring}.} are satisfied:
\begin{eqnarray*}
(a + b) + c &=& a + (b + c) \\
0 + a &=& a \\
a + 0 &=& a \\
a + b &=& b + a \\
(a \times b) \times c &=& a \times (b \times c) \\
1 \times a &=& a \\
a \times 1 &=& a \\
a \times (b + c) &=& (a \times b) + (a \times c) \\
(a + b) \times c &=& (a \times c) + (b \times c) \\
While we leave most proof details to the accompanying Coq code, it does seem important to introduce two key principles that are often implicit in proofs on paper.
The first is \emph{algebraic simplification}\index{algebraic simplification}, where we apply the defining equations of a recursive definition to simplify a goal.
For example, recall that our definition of expression size included this clause.
We may apply the defining equation to rewrite into a different formula, where we have essential pushed the definition of $\size{\cdot}$ through the $\mathsf{Plus}$.
We may use already-proved theorems via a more general \emph{rewriting}\index{rewriting} mechanism, applying whenever we know some quantified equality.
Within a new goal we are proving, we find some subterm that matches the lefthand side of that equality, after we choose the proper values of the quantified variables.
The process of finding those values automatically is called \emph{unification}\index{unification}.
Rewriting enables us to take the subterm we found and replace it with the righthand side of the equation.
As an example, assume that, for some $P$, we know $P(2+\size{\mathsf{Var}(x)})$ and are trying to prove $P(\size{\mathsf{Plus}(\mathsf{Var}(x), \mathsf{Const}(7))})$.
We may use our earlier fact to rewrite the argument of $P$ in what we are trying to show, so that it now matches the argument from what we already know, at which point the proof is trivial to finish.
Here, unification found the assignment $e =\mathsf{Var}(x)$.
We close the chapter with an important note on terminology.
A formula like $P(\size{\mathsf{Plus}(\mathsf{Var}(x), \mathsf{Const}(7))})$ combines several levels of notation.
We consider that we are doing our mathematical reasoning in some \emph{metalanguage}\index{metalanguage}, which is often applicable to a wide variety of proof tasks.
We also happen to be applying it here to reason about some \emph{object language}\index{object language}, a programming language whose syntax is defined formally, here the language of arithmetic expressions.
We have $x$ as a variable of the metalanguage, while $\mathsf{Var}(x)$ is a variable expression of the object language.
It is difficult to use English to explain the distinction between the two in complete formality, but be on the lookout for places where formulas mix concepts of the metalanguage and object language!
The general patterns should soon become clear, as they are somehow already familiar to us from natural-language sentences like:
\begin{quote}
The wise man said ``it is time to prove some theorems.''
\end{quote}
The quoted remark could just as well be in Spanish instead of English, in which case we have two languages nested in a nontrivial way.
We start at the top left, with a given expresson $e$ and valuation $v$.
The diagram shows the equivalence of \emph{two different paths} to the bottom right.
Each individual arrow is labeled with some description of the transformation it performs, to get from the term at its source to the term at its destination.
The right-then-down path is based on substituting and then interpreting, while the down-then-right path is based on extending the valuation and then interpreting.
Since both paths wind up at the same spot, the diagram indicates an equality between the corresponding terms.
It's a matter of taste whether the theorem statement or the diagram expresses the property more clearly!
As an example of a very different language, consider a \emph{stack machine}\index{stack machine}, similar at some level to, for instance, the Forth\index{Forth} programming language, or to various postfix\index{postfix} calculators.
Though here we defined an explicit grammar for programs, which are just sequences of instructions, in general we'll use the notation $\overline{X}$ to stand for sequences of $X$'s, and the associated concrete syntax won't be so important.
We also freely use single instructions to stand for programs, writing just $i$ in place of $i; \cdot$.
\newcommand{\push}[2]{#1 \rhd #2}
Each instruction of this language transforms a \emph{stack}\index{stack}, a last-in-first-out list of numbers.
Rather than spend more words on it, here is an interpreter that makes everythig precise.
Here and elsewhere, we overload the Oxford brackets $\denote{\ldots}$ shamelessly, where context makes clear which language or interpreter we are dealing with.
We write $s$ for stacks, and we write $\push{n}{s}$ for pushing number $n$ onto the top of stack $s$.
The last two cases require the stack have at least a certain height.
Here we'll ignore what happens when the stack is too short, though it suffices, for our purposes, to add pretty much any default behavior for the missing cases.
We overload $\denote{\overline{i}}$ to refer to the \emph{composition} of the interpretations of the different instructions within $\overline{i}$, in order.
Next, we give our first example of what might be called a \emph{compiler}\index{compiler}, or a translation from one language to another.
Let's compile arithmetic expressions into stack programs, which then become easy to map onto the instructions of common assembly languages.
In that sense, with this translation, we make progress toward efficient implementation on commodity hardware.
Throughout this book, we will use notation $\compile{\ldots}$ for compilation, where the floor-based notation suggests \emph{moving downward} to a lower abstraction level.
We strengthen the statement by considering both an arbitrary initial stack $s$ and a sequence of extra instructions $\overline{i}$ to be run after $e$.
The interpreter approach to semantics is usually the most convenient one, when it applies.
Coq requires that all programs terminate, and that requirement is effectively also present in informal math, though it is seldom called out with the same terms.
Instead, with math, we worry about whether recursive systems of equations are well-founded, in appropriate senses.
From either perspective, extra encoding tricks are required to write a well-formed interpreter for a Turing-complete\index{Turing-completeness} language.
We will dodge those complexities for now by defining a simple imperative language with bounded loops, where termination is easy to prove.
\textrm{Command}& c &::=&\mathsf{skip}\mid x \leftarrow e \mid c; c \mid\repet{e}{c}
\end{array}$$
Now the implicit state, read and written by a command, is a variable valuation, as we used in the interpreter for expressions.
A $\mathsf{skip}$ command does nothing, while $x \leftarrow e$ extends the valuation to map $x$ to the value of expression $e$.
We have simple command sequencing $c_1; c_2$, in addition to the bounded loop $\repet{e}{c}$, which executes $c$ a number of times equal to the value of $e$.
\newcommand{\id}[0]{\mathsf{id}}
To give the semantics, we need a few commonplace notations that are worth reviewing.
We write $\id$ for the identity function\index{identity function}, where $\id(x)= x$; and we write $f \circ g$ for composition of functions\index{composition of functions}$f$ and $g$, where $(f \circ g)(x)= f(g(x))$.
We also have iterated self-composition\index{self-composition}, written like \emph{exponentiation} of functions\index{exponentiation of functions}$f^n$, defined as follows.
\begin{eqnarray*}
f^0 &=&\id\\
f^{n+1}&=& f^n \circ f
\end{eqnarray*}
From here, $\denote{\ldots}$ is easy to define yet again, as a transformer over variable valuations.
To put this semantics through a workout, let's consider a simple \emph{optimization}\index{optimization}, a transformation whose input and output programs are in the same language.
There's an additional, fuzzier criterion for an optimization, which is that it should improve the program somehow, usually in terms of running time, memory usage, etc.
The optimization we choose here may be a bit dubious in that respect, though it is related to an optimization found in every serious C\index{C programming language} compiler.
In particular, let's tackle \emph{loop unrolling}\index{loop unrolling}.
When the iteration count of a loop is a constant $n$, we can replace the loop with $n$ sequenced copies of its body.
C compilers need to work harder to find the iteration count of a loop, but luckily our language includes loops with very explicit iteration counts!
To define the transformation, we'll want a recursive function and notation for sequencing of $n$ copies of a command $c$, written $^nc$.
\begin{eqnarray*}
^0c &=&\mathsf{skip}\\
^{n+1}c &=& c; {^nc}
\end{eqnarray*}
\newcommand{\opt}[1]{{\left | #1 \right |}}
Now the optimization itself is easy to define.
We'll write $\opt{\ldots}$ for this and other optimizations, which move neither down nor up a tower of program abstraction levels.
Note that, when multiple defining equations apply to some function input, by convention we apply the \emph{earliest} equation that matches.
Let's prove that this optimization preserves program behavior; that is, we prove that it is \emph{semantics preserving}\index{semantics preservation}.
\begin{theorem}\label{unroll}
$\denote{\opt{c}}v =\denote{c}v$.
\end{theorem}
It all looks so straightforward from that statement, doesn't it?
Indeed, there actually isn't so much work to do to prove this theorem.
We can also present it as a commuting diagram much like the prior one.
\[
\begin{tikzcd}
c \arrow{r}{\opt{\ldots}}\arrow{dr}{\denote{\ldots}}&\opt{c}\arrow{d}{\denote{\ldots}}\\
&\denote{c}
\end{tikzcd}
\]
The statement of Theorem \ref{unroll} happens to already be in the right form to do induction directly, but we need a helper lemma, capturing the interaction of $^nc$ and the semantics.
\begin{lemma}
$\denote{^nc}=\denote{c}^n$.
\end{lemma}
Let us end the chapter with the commuting-diagram version of the lemma statement.
\[
\begin{tikzcd}
c \arrow{r}{^n\ldots}\arrow{d}{\denote{\ldots}}&^nc \arrow{d}{\denote{\ldots}}\\
For simple programming languages where programs always terminate, it is often most convenient to formalize them using interpreters, as in the last chapter.
However, many important languages don't fall into that category, and for them we need different techniques.
Nontermination isn't always a bug; for instance, we expect a network server to run indefinitely.
We still need to be able to talk about the correct behavior of programs that run forever, by design.
For that reason, in this chapter and in most of the rest of the book, we model programs using relations, in much the same way that may be familiar from automata theory\index{automata theory}.
An important difference, though, is that, while undergraduate automata-theory classes generally study \emph{finite-state machines}\index{finite-state machines}, for general program reasoning we want to allow infinite sets of states, otherwise referred to as \emph{infinite-state systems}\index{infnite-state systems}.
Let's start with an example that almost seems too mundane to be associated with such terms.
\section{Factorial as a State Machine}
We're familiar with the factorial operation, implemented as an imperative program with a loop.
\begin{verbatim}
factorial(n) {
a = 1;
while (n > 0) {
a = a * n;
n = n - 1;
}
return a;
}
\end{verbatim}
In the analysis to follow, consider some value $n_0\in\mathbb N$ fixed, as the input passed to this operation.
A state machine is lurking within the surface syntax of the program.
For consistency with the notation we will be using later, we define the set $\mathcal F_0$ using an inference rule.
Equivalently, we could just write $\mathcal F_0=\{\mathsf{WithAccumulator}(n_0, 1)\}$, essentially reading off the initial variable values from the first lines of the code above.
Similarly, we also define a set of \emph{final states}\index{final state}.
Note that this definition only captures when the program is \emph{done}, not when it \emph{returns the right answer}.
It follows from the last line of the code.
The last and most important ingredient of our state machine is its \emph{transition relation}, where we write $s \to s'$ to indicate that state $s$ advances to state $s'$ in one step, following the semantics of the program.
Here inference rules are more obviously a good fit.
$$\infer{\mathsf{WithAccumulator}(n+1, a)\to\mathsf{WithAccumulator}(n, a \times(n+1))}{}$$
The first rule corresponds to the case where the program ends, because the loop test has failed and we now know the final answer.
The second rule corresponds to going once around the loop, following directly from the code in the loop body.
We can fit these ingredients into the general concept of a \emph{transition system}\index{transition system}, the term we will use throughout this book for this sort of state machine.
Actually, the words ``state machine'' suggest to many people that the state set must be finite, hence our preference for ``transition system,'' which is also used fairly frequently in semantics.
A \emph{transition system} is a triple $\angled{S, S_0, \to}$, with $S$ a set of states, $S_0\subseteq S$ a set of initial states, and $\to\;\subseteq S \times S$ a transition relation.
\end{definition}
For an arbitrary transition relation $\to$, not just the one defined above for factorial, we define its \emph{transitive-reflexive closure}\index{transitive-reflexive closure}$\to^*$ with two inference rules:
$$\infer{s \to^* s}{}
\quad\infer{s \to^* s''}{
s \to s'
& s' \to^* s''
}$$
That is, a formal claim $s \to^* s'$ corresponds exactly to the informal claim that ``starting from state $s$, we can reach state $s'$.''
\begin{definition}
For transition system $\angled{S, S_0, \to}$, we say that a state $s$ is \emph{reachable} if and only if there exists $s_0\in S_0$ such that $s_0\to^* s$.
\end{definition}
Building on these notations, here is one way to state the correctness of our factorial program, which, defining $S$ according to the state grammar above, we model as $\mathcal F =\angled{S, \mathcal F_0, \to}$.
The concept of ``invariant'' may be familiar from such relatively informal notions as ``loop invariant''\index{loop invariant} in introductory programming classes.
Intuitively, an invariant is a property of program state that \emph{starts true and stays true}, but let's make that idea a bit more formal, as applied to our transition-system formalism.
An \emph{invariant} of a transition system is a property that is always true, in all reachable states of a transition system. That is, for transition system $\angled{S, S_0, \to}$, where $R$ is the set of all its reachable states, some $I \subseteq S$ is an invariant iff $R \subseteq I$.
\end{definition}
At first look, the definition may appear a bit silly.
Why not always just take the reachable states $R$ as the invariant, instead of scrambling to invent something new?
The reason is the same as for strengthening induction hypotheses to make proofs easier.
Often it is easier to characterize an invariant that isn't fully precise, admitting some states that the system can never actually reach.
Consider a transition system $\angled{S, S_0, \to}$ and its candidate invariant $I$. The candidate is truly an invariant if (1) $S_0\subseteq I$ and (2) for every $s \in I$ where $s \to s'$, we also have $s' \in I$.
I(\mathsf{WithAccumulator}(n, a)) &=& n_0! = n! \times a
\end{eqnarray*}
It is an almost-routine exercise to prove that $I$ really is an invariant, using Theorem \ref{invariant_induction}.
The key new ingredient we need is \emph{inversion}, a principle for deducing which inference rules may have been used to prove a fact.
For instance, at one point in the proof, we need to draw a conclusion from a premise $s \in\mathcal F_0$, meaning that $s$ is an initial state.
By inversion, because set $\mathcal F_0$ is defined by a single inference rule, that rule must have been used to conclude the premise, so it must be that $s =\mathsf{WithAccumulator}(n_0, 1)$.
The relation $\to$ is defined by two inference rules, so inversion leads us to two cases to consider.
In the first case, corresponding to the first rule, $s =\mathsf{WithAccumulator}(0, a)$ and $s' =\mathsf{AnswerIs}(a)$.
In the second case, corresponding to the second rule, $s =\mathsf{WithAccumulator}(n+1, a)$ and $s' =\mathsf{WithAccumulator}(n, a \times(n+1))$.
It's worth checking that these values of $s$ and $s'$ are read off directly from the rules.
Though a completely formal and exhaustive treatment of inversion is beyond the scope of this text, generally it follows standard intuitions about ``reverse-engineering'' a set of rules that could have been used to derive some premise.
Another important property of invariants formalizes the connection with weakening an induction hypothesis.
\begin{theorem}\label{invariant_weaken}
If $I$ is an invariant of a transition system, then $I' \supseteq I$ (a superset of the original) is also an invariant of the same system.
\end{theorem}
Note that the larger $I'$ above may not be suitable to use in an inductive proof by Theorem \ref{invariant_induction}!
For instance, for factorial, we might define $I' =\mathcal\{\mathsf{AnswerIs}(n_0!)\}\cup\{\mathsf{WithAccumulator}(n, a)\mid n, a \in\mathbb N\}$, clearly a superset of $I$.
However, by forgetting everything that we know about intermediate $\mathsf{WithAccumulator}$ states, we will get stuck on the inductive step of the proof.
Thus, what we call invariants here needn't also be \emph{inductive invariants}\index{inductive invariants}, and there may be slight terminology mismatches with other sources.
Combining Theorems \ref{invariant_induction} and \ref{invariant_weaken}, it is now easy to prove Theorem \ref{factorial_ok}, establishing the correctness of our particular factorial system $\mathcal F$.
First, we use Theorem \ref{invariant_induction} to deduce that $I$ is an invariant of $\mathcal F$.
Then, we choose the very same $I'$ that we warned above is not an inductive invariant, but which is fairly easily shown to be a superset of $I$.
Therefore, by Theorem \ref{invariant_weaken}, $I'$ is also an invariant of $\mathcal F$, and Theorem \ref{factorial_ok} follows quite directly from that fact, as $I'$ is essentially a restatement of Theorem \ref{factorial_ok}.
Another crucial reasoning technique was hidden within the elided proof of Theorem \ref{invariant_induction}.
That technique is \emph{rule induction}\index{rule induction}, which generalizes inversion just as normal structural induction generalizes case analysis.
As an example, consider again the definition of transitive-reflexive closure by inference rules.
We can actually derive a suitable induction principle, in the same way that we produced structural induction principles from definitions of inductive datatypes.
We modify each defining rule of $\to^*$, replacing its conclusion with a use of $P$ and adding a $P$ induction hypothesis for each recursive premise.
$$\infer{P(s, s)}{}
\quad\infer{P(s, s'')}{
s \to s'
& s' \to^* s''
& P(s', s'')
}$$
As before, where the defining rules of $\to^*$ show us how to \emph{conclude} facts, the two new rules here are \emph{proof obligations}.
To apply rule induction and establish $P$ for all reachability pairs, we must prove that each new rule is correct, as a kind of quantified implication.
As a simpler example than the invariant-induction theorem, consider transitivity for reachability.
\begin{theorem}
If $s \to^* s'$ and $s' \to^* s''$, then $s \to^* s''$.
\end{theorem}
\begin{proof}
By rule induction on the derivation of $s \to^* s'$, taking $P(s_1, s_2)$ to be that, if $s_2= s'$, then $s_1\to^* s''$. We consider variables $s'$ and $s''$ fixed throughout the induction, along with their associated premise $s' \to^* s''$.
\emph{Base case:} We must show $P(s, s)$ for an arbitrary $s$. Given that (based on the definition of $P$) we may assume $s = s'$, our premise $s' \to^* s''$ precisely matches the desired conclusion $s \to^* s''$.
\emph{Induction step:} Assume $s \to s_1$, $s_1\to^* s'$, and $P(s_1, s')$. We may apply the second rule defining $\to^*$, whose two premises become $s \to s_1$ and $s_1\to^* s''$. The first is one of the available premises of the induction step. The second follows by the induction hypothesis about $P$.
\end{proof}
This sort of proof really is easier to follow in Coq code, so we especially encourage the reader to consult the mechanized version here!
In general, any inductive definition of a predicate, via a set of inference rules, implies a rule-induction principle.
We will meet many such definitions throughout the book, and we will apply rule induction to most of them.
It is valuable to understand basically how the rule-induction principle of a definition is read off from its original rules, but it is also true that Coq comes up with these principles automatically.
\section{An Example with a Concurrent Program}
Imagine that we want to verify a multithreaded\index{multithreaded programs}, shared-memory program\index{shared-memory programming} where multiple threads run this code at once.
\begin{verbatim}
f() {
lock();
local = global;
global = local + 1;
unlock();
}
\end{verbatim}
Consider \texttt{global} as a variable shared across all threads, while each thread has its own version of variable \texttt{local}.
The meaning of \texttt{lock()} and \texttt{unlock()} is as usual\index{locks}, where at most one thread can hold the lock at once, claiming it via \texttt{lock()} and relinquishing it via \texttt{unlock()}.
When variable \texttt{global} is initialized to 0 and $n$ threads run this code at once and all terminate, we expect that \texttt{global} finishes with value $n$.
Of course, bugs in this program, like forgetting to include the locking, could lead to all sorts of wrong answers, with any value between 1 and $n$ possible with the right demonic thread interleaving.
\encoding
To prove that we got the program right, let's formalize it as a transition system. First, our state set:
$$\begin{array}{rrcl}
\textrm{States}& S &::=&\mathsf{Lock}\mid\mathsf{Read}\mid\mathsf{Write}(n) \mid\mathsf{Unlock}\mid\mathsf{Done}
\end{array}$$
Compared to the last example, here we see more clearly that kinds of states correspond to \emph{program counters}\index{program counters} in the imperative code.
The first four state kinds respectively mean that the program counter is right before the matching line in the program's code.
The last state kind means the program counter is past the end of the function.
Only $\mathsf{Write}$ states carry extra information, in this case the value of variable \texttt{local}.
At every other program counter, we can prove that the value of variable \texttt{local} has no effect on further transitions, so we don't bother to store it.
We will account for the value of variable \texttt{global} separately, in a way to be described shortly.
In particular, we will define a transition system for a single thread as $\mathcal L =\angled{(\mathbb N \times\mathbb B)\times S, \mathcal L_0, \to_{\mathcal L}}$.
We define the state to include not only the thread-local state $S$ but also the value of \texttt{global} (in $\mathbb N$) and whether the lock is currently taken (in $\mathbb B$, the Booleans, with values $\top$ [true] and $\bot$ [false]).
Note that these rules will allow a thread to read and write the shared state even without holding the lock.
The rules also allow any thread to unlock the lock, with no consideration for whether that thread must be the current lock holder.
We must use an invariant-based proof to show that there are, in fact, no lurking violations of the lock-based concurrency discipline.
Of course, with just a single thread running, there aren't any interesting violations!
However, we have been careful to describe system $\mathcal L$ in a generic way, with its state a pair of shared and private components.
We can define a generic notion of a multithreaded system, with two systems that share some state and maintain their own private state.
\encoding
\begin{definition}
Let $T^1=\angled{S \times P^1, S_0\times P^1_0, \to^1}$ and $T^2=\angled{S \times P^2, S_0\times P^2_0, \to^2}$ be two transition systems, with a shared-state type $S$ in common between their state sets, also agreeing on the initial values $S_0$ for that shared state. We define the \emph{parallel composition}$T^1\mid T^2$ as $\angled{S \times(P^1\times P^2), S_0\times(P^1_0\times P^2_0), \to}$, defining new transition relation $\to$ with the following inference rules, which capture the usual notion of thread interleaving.
Note that the operator $\mid$ is carefully defined so that its output is suitable as input to a further instance of itself.
As a result, while $\mathcal L \mid\mathcal L$ is a transition system modeling two threads running the code from above, we also have $\mathcal L \mid(\mathcal L \mid\mathcal L)$ as a three-thread system based on that code, $(\mathcal L \mid\mathcal L)\mid(\mathcal L \mid\mathcal L)$ as a four-thread system based on that code, etc.
Also note that $\mid$ constructs transition systems with our first examples of \emph{nondeterminism}\index{nondeterminism} in transition relations.
That is, given a particular starting state, there are multiple different places it may wind up after a given number of execution steps.
In general, with thread-interleaving concurrency, the set of possible final states grows exponentially in the number of steps, a fact that torments concurrent-software testers to no end!
Rather than consider all possible runs of the program, we will use an invariant to tame the complexity.
First, we should be clear on what we mean to prove about this program.
Let's also restrict our attention to the two-thread case for the rest of this section; the $n$-thread case is left as an exercise for the reader!
\begin{theorem}
For any reachable state $((\ell, g), (p^1, p^2))$ of $\mathcal L \mid\mathcal L$, if $p^1= p^2=\mathsf{Done}$, then $g =2$.
\end{theorem}
That is, when both threads terminate, \texttt{global} equals 2.
As a first step toward an invariant, define function $\mathcal C$ from private states to numbers, capturing the \emph{contribution of} a thread with that state, summarizing how much that thread has added to \texttt{globals}.
\begin{eqnarray*}
\mathcal C(p) &=&\begin{cases}
1 & p \in\{\mathsf{Unlock}, \mathsf{Done}\}\\
0 &\mathrm{otherwise}
\end{cases}
\end{eqnarray*}
Next, we define a function that, given a thread's private state, determines whether that thread \emph{holds the lock}.
\begin{eqnarray*}
\mathcal H(p) &=&\begin{cases}
\bot& p \in\{\mathsf{Lock}, \mathsf{Done}\}\\
\top&\mathrm{otherwise}
\end{cases}
\end{eqnarray*}
Now, the main insight: we can reconstruct the shared state uniquely from the two private states!
One last ingredient will help us write the invariant: a predicate $\mathcal O(p, p')$ capturing when, given the state $p$ of one thread, the state $p'$ is compatible with all of the implications of $p$'s state, primarily in terms of mutual exclusion\index{mutual exclusion} for the lock.
\begin{eqnarray*}
\mathcal O(p, p') &=&\begin{cases}
\top& p \in\{\mathsf{Lock}, \mathsf{Done}\}\\
\neg\mathcal H(p') & p \in\{\mathsf{Read}, \mathsf{Unlock}\}\\
\neg\mathcal H(p') \land n = \mathcal C(p') & p = \mathsf{Write}(n)
As is often the case, defining the invariant is the hard part of the proof, and the rest follows by the standard methodology that we used for factorial.
To recap that method, first we use Theorem \ref{invariant_induction} to show that $I$ really is an invariant of $\mathcal L \mid\mathcal L$.
Next, we use Theorem \ref{invariant_weaken} to show that $I$ implies the original property of interest, that finished program states have value 2 for \texttt{global}.
Most of the action is in the first step, where we must work through fussy details of all the different steps that could happen from a state within the invariant, using arithmetic reasoning in each case to either derive a contradiction (that step couldn't happen from this starting state) or show that a specific new state also belongs to the invariant.
We leave those details to the Coq code, as usual.
The reader may be worried at this point that coming up with invariants can be rather tedious!
In the next chapter, we meet a technique for finding invariants automatically, in some limited but important circumstances.
Our analyses so far have been tedious for at least two different reasons.
First, we've hand-crafted definitions of transition systems, rather than just writing programs in conventional programming languages.
The next chapter will clear that obstacle, by introducing operational semantics, for building transition systems automatically from programs.
The other inconvenience we've faced is defining invariants manually.
There isn't a silver bullet to get us out of this duty, when working with Turing-complete languages\index{Turing-completeness}, where almost all interesting questions, this one included, are undecidable.
However, when we can phrase problems in terms of transition systems with \emph{finitely many reachable states}, we can construct invariants automatically by \emph{exhaustive exploration of the state space}, an approach otherwise known as \emph{model checking}\index{model checking}.
Surprisingly many real programs can be reduced to finite state spaces, using the techniques introduced in this chapter.
First, though, let's formalize our intuitions about exhaustive state-space exploration as a sound way to find invariants.
\section{Exhaustive Exploration}
For an arbitrary binary relation $R$, we write $R^n$ for the $n$-times self-composition of $R$\index{self-composition of relations}.
Formally, where $\mathsf{id}$ is the identity relation\index{identity relation} that only relates values to themselves, we have:
\begin{eqnarray*}
R^0 &=&\mathsf{id}\\
R^{n+1}&=& R \circ R^n
\end{eqnarray*}
For some set $S$ and binary relation $R$, we also write $R(S)$ for the composition of $R$ and $S$\index{composition of a relation and a set}, namely $\{x \mid\exists y \in S. \; y \; R \; x\}$.
\newcommand{\ns}[0]{\hspace{-.05in}}
Which states of transition system $\angled{S, S_0, \to}$ are reachable after 0 steps?
That would be precisely the initial states $S_0$, which we can also write as $\to^0\ns(S_0)$.
Which states are reachable after exactly 1 step?
That is $\to\ns(S_0)$, or $\to^1\ns(S_0)$.
How about 2, 3, and 4 steps?
There we have $\to^2\ns(S_0)$, $\to^3\ns(S_0)$, and $\to^4\ns(S_0$).
It follows that the set of states reachable after $n$ steps is:
\begin{eqnarray*}
\mathsf{reach}(n) &=&\bigcup_{i < n}\to^i\ns(S_0)
\end{eqnarray*}
This iteration process is not obviously executable yet, because, a priori, we seem to need to consider all possible $n$ values, to characterize the state space fully.
However, a crucial property allows us to terminate our search soundly under some conditions.
\begin{theorem}
\invariants
If $\mathsf{reach}(n+1)=\mathsf{reach}(n)$ for some $n$, then $\mathsf{reach}(n)$ is an invariant of the system.
\end{theorem}
Here we call $\mathsf{reach}(n)$ a \emph{fixed point}\index{fixed point} of the transition system, because it is closed under further exploration.
To find a fixed point with a concrete system, we start with $S_0$.
We repeatedly take the \emph{single-step closure}\index{single-step closure} corresponding to composition with $\to$.
At each step, we check whether the expanded set is actually equal to the previous set.
If so, our process of \emph{multi-step closure}\index{multi-step closure} has terminated, and we have an invariant, by construction.
Again, keep in mind that multi-step closure will not terminate for most transition systems, and there is an art to phrasing a problem in terms of systems where it \emph{will} terminate.
When analyzing an infinite-state system, it is not necessary to give up hope for model checking.
For instance, consider this program.
\begin{verbatim}
int global = 0;
thread() {
int local;
while (true) {
local = global;
global = local + 2;
}
}
\end{verbatim}
If we assume infinite-precision integers, then the state space is infinite.
Considering just the global variable, every even number is reachable, even if we only run a single thread.
However, there is a high degree of regularity across this state space.
In particular, those values really are all even.
Consider this other program, which is hauntingly similar to the last one, in a way that we will make precise shortly.
\begin{verbatim}
bool global = true;
thread() {
bool local;
while (true) {
local = global;
global = local;
}
}
\end{verbatim}
We replaced every use of an integer with \emph{a Boolean that is true iff the integer is even}.
Notice that now the program has a finite state space, and model checking applies easily!
We can formalize such a transformation via the general principle of \emph{abstraction of a transition system}\index{abstraction}.
\newcommand{\simulate}[0]{\prec}
The key idea is that every state of the concrete system (with relatively many states) can be associated to one or more states of the abstract system (with relatively few states).
We formalize this association via a \emph{simulation relation}\index{simulation relation}$R$, and we define what makes a choice of $R$ sound, via a notion of \emph{simulation}\index{simulation} via a binary operator $\simulate$, subscripted by $R$.
(\forall s \in S_0. \;\exists s' \in S'_0. \; s \; R \; s')
& (\forall s, s', s_1. \; s \; R \; s' \land s \to s_1 \Rightarrow\exists s'_1. \; s' \to' s'_1 \land s_1 \; R \; s'_1)
}$$
The simpler condition is that every concrete initial state must be related to at least one abstract initial state.
The second, more complex condition essentially says that every step in the concrete world must be matchable by some related step in the abstract world.
A commuting diagram may express the second condition more clearly.
\[
\begin{tikzcd}
s \arrow{r}{\to}\arrow{d}{R}& s_1 \arrow{d}{R}\\
s' \arrow{r}{\exists\to'}& s'_1
\end{tikzcd}
\]
At an even higher intuitive level, what simulation says is that every execution of the concrete system may be matched, step for step, by an execution of the abstract system.
The relation $R$ explains the rules for which states match across systems.
For our purposes, the key pay-off from this connection is that we may translate any invariant of the abstract system into an invariant of the concrete system.
If $\angled{S, S_0, \to}\simulate_R \angled{S', S'_0, \to'}$, and if $I$ is an invariant of $\angled{S', S'_0, \to'}$, then $R^{-1}(I)$ is an invariant of $\angled{S, S_0, \to}$.
\end{theorem}
We can apply this theorem to the two example programs from earlier in the section.
The concrete system can be represented with thread-local states $\{\mathsf{Read}\}\cup\{\mathsf{Write}(n)\mid n \in\mathbb N\}$ and the abstract system with $\{\mathsf{BRead}\}\cup\{\mathsf{BWrite}(b)\mid b \in\mathbb B\}$, for the Booleans $\mathbb B$.
n \;\textrm{even}\Leftrightarrow b = \mathsf{true}
}$$
We also define the overall state simulation relation $R$, which also covers state shared by threads.
$$\infer{(n, (\ell_1, \ell_2))\; R \;(b, (\ell'_1, \ell'_2))}{
(n \;\textrm{even}\Leftrightarrow b = \mathsf{true})
&\ell_1 \sim\ell'_1
&\ell_2 \sim\ell'_2
}$$
By proving that $R$ is truly a simulation relation, we reduce the problem to finding an invariant for the abstract system, which is easy to do with model checking.
One crucial consequence of abstraction-by-simulation deserves mentioning:
We show that every concrete execution is matched abstractly, but there may also be additional abstract executions that don't match any concrete ones.
In model checking the abstract system, we may do extra work to handle these ``useless'' paths!
If we do manage to handle them all, then Theorem \ref{abstract_simulation} applies perfectly well.
However, we should be careful, in our choices of abstractions, to bias our designs toward those that don't introduce extra complexities.
\section{Modular Decomposition of Invariant-Finding}
Many transition systems are straightforward to abstract into others, as single global steps.
Other times, the right way to tame a complex system is to decompose it into others and analyze them separately for invariants.
In such cases, the key is a proof principle to combine the invariants of the component systems into an invariant of the overall system.
We will refer to this style of proof decomposition as \emph{modularity}\index{modularity}, and this section gives our first example of modularity, for multithreaded systems.
Imagine that we have a system consisting of $n$ different copies of a transition system $\angled{S, S_0, \to}$ running as concurrent threads, modeled in the way introduced in the previous chapter.
It's not obvious that we can analyze each thread separately, since, during that thread's execution, the other threads are constantly interrupting and modifying global state.
To make matters worse, we can only understand their patterns of state modification by analyzing their thread-local state.
The situation seems inherently unmodular.
However, consider the following construction on transition systems.
Given a transition relation $\to$ and an invariant $I$ on the global state shared by all threads, we define a new transition relation $\to^I$ as follows.
$$\infer{s \to^I s'}{
s \to s'
}
\quad\infer{(g, \ell) \to^I (g', \ell)}{
I(g')
}$$
The first rule says that any step of the original relation is also a step of the new relation.
However, the second rule adds a new kind of step: the global state may change \emph{arbitrarily}, so long as the new value satisfies invariant $I$.
We lift this operation to full transition systems, defining $\angled{S, S_0, \to}^I =\angled{S, S_0, \to^I}$.
This construction trivially acts as an abstraction.
\begin{theorem}\label{shared_invariant_abstract}
\abstraction
$\mathbb S \simulate_\mathsf{id}{\mathbb S}^I$, for any system $\mathbb S$ and property $I$.
However, we wouldn't want to make this abstraction step in a proof about a single thread.
We needlessly complicate our model checking by forcing ourselves to consider all modifications of the global state that obey $I$.
The payoff comes in analyzing multithreaded systems.
\begin{theorem}\label{shared_invariant_modular}
\modularity
Where $I$ is an invariant over only the shared state of a multithreaded system, let $I' =\{(g, \ell)\mid I(g)\}$ be the lifting of $I$ to cover full states, local parts included. If $I'$ is an invariant for both ${\mathbb S}_1^I$ and ${\mathbb S}_2^I$, then $I'$ is also an invariant for $({\mathbb S}_1\mid{\mathbb S}_2)^I$.
\end{theorem}
This theorem gives us a way to analyze the threads in a system separately.
As an example, consider this program, where multiple threads will run \texttt{f()} simultaneously.
\begin{verbatim}
int global = 0;
f() {
int local = 0;
while (true) {
local = global;
local = 3 + local;
local = 7 + local;
global = local;
}
}
\end{verbatim}
Call the transition-system encoding of this code $\mathbb S$.
We can apply the Boolean-for-evenness abstraction to model a single thread with finite state, but we are left needing to account for interference by other threads.
However, we can apply Theorem \ref{shared_invariant_modular} to analyze threads separately.
For instance, we want to show that ``\texttt{global} is always even'' is an invariant of ${\mathbb S}\mid{\mathbb S}$.
By Theorem \ref{shared_invariant_abstract}, we can switch to analyzing system $({\mathbb S}\mid{\mathbb S})^I$, where $I$ is the evenness invariant.
By Theorem \ref{shared_invariant_modular}, we can switch to proving the same invariant separately for systems ${\mathbb S}^I$ and ${\mathbb S}^I$, which are, of course, the same system in this case.
We apply the Boolean-for-evenness abstraction to this system, to get one with a finite state space, so we can check the invariant automatically by model checking.
Following the chain of reasoning backward, we have proved the invariant for ${\mathbb S}\mid{\mathbb S}$.
Even better, that last proof includes the hardest steps that carry over to the proof for an arbitrary number of threads.
Define an exponentially growing system of threads ${\mathbb S}^n$ by:
For any $n$, it is an invariant of ${\mathbb S}^n$ that the global variable is always even.
\end{theorem}
\begin{proof}
By induction on $n$, repeatedly using Theorem \ref{shared_invariant_modular} to push the obligation down to the leaves of the tree of concurrent compositions, after applying Theorem \ref{shared_invariant_abstract} at the start to introduce the use of $\ldots^I$.
Every leaf is the same system $\mathbb S$, for which we abstract and apply model checking, appealing to the step above where we ran the same analysis.
It gets tedious to define a relation from first principles, to explain the behaviors of any concrete program.
We do more things with programs than just reason about them.
For instance, we compile them into other languages.
To get the most mileage out of our correctness proofs, we should connect them to the same program syntax that we pass to compilers.
\emph{Operational semantics}\index{operational semantics} is a family of techniques for automatically defining a transition system, or other relational characterization, from program syntax.
For our example language, we define a relation written $\bigstep{(v, c)}{v'}$, for ``command $c$, run with variable valuation $v$, terminates, modifying the valuation to $v'$.''
Notice how the definition is quite similar to a recursive interpreter\index{interpreters} written in a high-level programming language, though we write with the language of relations instead of functional programming.
For instance, consider the simple case of the rule for sequencing, ``;''.
We first ``call the interpreter'' on the first subcommand $c_1$ with the original valuation $v$.
The result of the ``recursive call'' is a new valuation $v_1$, which we then feed into another ``recursive call'' on $c_2$, whose result becomes the overall result.
Why write this interpreter relationally instead of as a functional program?
The most relevant answer applies to situations like ours as users of Coq or even of informal mathematics, where we must be very careful that all of our recursive definitions are well-founded.
The recursive version of this relation is clearly not well-founded, as it would run forever on a nonterminating $\mathsf{while}$ loop.
It is also easier to incorporate \emph{nondeterminism}\index{nondeterminism} in the relational style, a possibility that we will return to at the end of the chapter.
The big-step semantics is easy to apply to concrete programs.
For instance, define $\mathtt{factorial}$ as the program $\assign{\mathtt{output}}{1}; \while{\mathtt{input}}{(\assign{\mathtt{output}}{\mathtt{output}\times\mathtt{input}}; \assign{\mathtt{input}}{\mathtt{input}-1})}$.
\begin{theorem}
There exists $v$ such that $\bigstep{(\mupd{\mempty}{\mathtt{input}}{2}, \mathtt{factorial})}{v}$ and $\msel{v}{\mathtt{output}}=2$.
\end{theorem}
\begin{proof}
By repeated application of the big-step inference rules.
\end{proof}
We can even prove that $\mathtt{factorial}$ behaves correctly on all inputs, by way of a lemma about $\mathtt{factorial\_loop}$ defined as $\while{\mathtt{input}}{(\assign{\mathtt{output}}{\mathtt{output}\times\mathtt{input}}; \assign{\mathtt{input}}{\mathtt{input}-1})}$.
\begin{lemma}\label{factorial_loop}
If $\msel{v}{\mathtt{input}}= n$ and $\msel{v}{\mathtt{output}}= o$, then there exists $v'$ such that $\bigstep{(v, \mathtt{factorial\_loop})}{v'}$ and $\msel{v'}{\mathtt{output}}= n!\times o$.
\end{lemma}
\begin{proof}
By induction on $n$.
\end{proof}
\begin{lemma}
If $\msel{v}{\mathtt{input}}= n$, then there exists $v'$ such that $\bigstep{(v, \mathtt{factorial})}{v'}$ and $\msel{v'}{\mathtt{output}}= n!$.
\end{lemma}
\begin{proof}
Largely by direct appeal to Lemma \ref{factorial_loop}.
\end{proof}
Most of our program proofs in this book establish \emph{safety properties}\index{safety properties}, or invariants of transition systems.
However, these last two examples with big-step semantics also establish program termination, taking us a few steps into the world of \emph{liveness properties}\index{liveness properties}.
Often it is convenient to break a system's execution into small sequential steps, rather than executing a whole program in one go.
Perhaps the most compelling example comes from concurrency, where it is difficult to give a big-step semantics directly.
Nonterminating programs are the other standard example.
We want to be able to establish invariants for those programs, all the same, and we need a semantics to help us state what it means to be an invariant.
\newcommand{\smallstep}[2]{#1 \to #2}
The canonical solution is \emph{small-step operational semantics}\index{small-step operational semantics}, probably the most common approach to formal program semantics in contemporary research.
Now we define a single-step relation $\smallstep{(v, c)}{(v', c')}$, meaning that one execution step transforms the first state into the second state.
Each state is a valuation $v$ and a current command $c$.
The intuition behind the rules may come best from working out an example.
\newcommand{\smallsteps}[2]{#1 \to^* #2}
\begin{theorem}
There exists valuation $v$ such that $\smallsteps{(\mupd{\mempty}{\mathtt{input}}{2}, \mathtt{factorial})}{(v, \skipe)}$ and $\msel{v}{\mathtt{output}}=2$.
\end{theorem}
\begin{proof}
Here is a step-by-step (literally!) derivation that finds $v$.
Clearly the final valuation assigns $\mathtt{output}$ to 2.
\end{proof}
\subsection{Equivalence of Big-Step and Small-Step}
Different theorems are easier to prove with different semantics, so it is helpful to establish formally the intuitive connection between big and small steps.
\begin{lemma}
If $\smallsteps{(v, c_1)}{(v', c'_1)}$, then $\smallsteps{(v, c_1; c_2)}{(v', c'_1; c_2)}$,
\end{lemma}
\begin{proof}
By induction on the derivation of $\smallsteps{(v, c_1)}{(v', c'_1)}$.
\end{proof}
\begin{theorem}
If $\bigstep{(v, c)}{v'}$, then $\smallsteps{(v, c)}{(v', \skipe)}$.
\end{theorem}
\begin{proof}
By induction on the derivation of $\bigstep{(v, c)}{v'}$, appealing to the last lemma at two points.
\end{proof}
\begin{lemma}
If $\smallstep{(v, c)}{(v', c')}$ and $\bigstep{(v', c')}{v''}$, then $\bigstep{(v, c)}{v''}$. In other words, we can add a small step to the beginning of any big-step derivation.
\end{lemma}
\begin{proof}
By induction on the derivation of $\smallstep{(v, c)}{(v', c')}$.
\end{proof}
\begin{lemma}
If $\smallsteps{(v, c)}{(v', c')}$ and $\bigstep{(v', c')}{v''}$, then $\bigstep{(v, c)}{v''}$. In other words, we can add any number of small steps to the beginning of any big-step derivation.
\end{lemma}
\begin{proof}
By induction on the derivation of $\smallsteps{(v, c)}{(v', c')}$, appealing to the last lemma.
\end{proof}
\begin{theorem}
If $\smallsteps{(v, c)}{(v', \skipe)}$, then $\bigstep{(v, c)}{v'}$.
\end{theorem}
\begin{proof}
Largely by appeal to the last lemma, considering that $\bigstep{(v', \skipe)}{v'}$.
\end{proof}
\subsection{Transition Systems from Small-Step Semantics}
The small-step semantics is a natural fit with our working definition of transition systems.
We can define a transition system from any valuation and command, where $\mathbb V$ is the set of valuations and $\mathbb C$ the set of commands, by $\mathbb T(v, c)=\angled{\mathbb V \times\mathbb C, \{(v, c)\}, \to}$.
Given even $n$, for $\mathbb T(\mupd{\mupd{\mempty}{\mathtt{n}}{n}}{\mathtt{a}}{0}, P)$, it is an invariant that the valuation maps variable $\mathtt{a}$ to an even number.
Our strengthened invariant is $I(v, c)= c \in\overline{P}\land(\exists n. \;\msel{v}{\mathtt{n}}= n \land\textrm{even}(n))\land(\exists a. \;\msel{v}{\mathtt{a}}= a \land\textrm{even}(a))$.
In other words, we strengthen by adding the constraints that (1) we do not stray from the expected set of reachable commands and (2) variable \texttt{n} also remains even.
The strengthened invariant is straightforward to prove by invariant induction, using repeated inversion on $\to$ facts.
This rule is an example of a \emph{congruence rule}\index{congruence rule}, which shows how to take a step and \emph{lift} it into a step within a larger command, whose other subcommands are unaffected.
Complex languages can require many congruence rules, and yet we feel like we should be able to avoid repeating all this boilerplate logic somehow.
A common way to do so is switching to \emph{contextual small-step semantics}\index{contextual small-step semantics}.
The first step is to define a set of \emph{evaluation contexts}\index{evaluation contexts}, which formalize the spots within a larger command where steps are enabled.
\textrm{Evaluation contexts}& C &::=&\Box\mid C; c
\end{array}$$
\newcommand{\plug}[2]{#1[#2]}
We define the operator of \emph{plugging}\index{plugging evaluation contexts} an evaluation context in the natural way.
\begin{eqnarray*}
\plug{\Box}{c}&=& c \\
\plug{(C; c_2)}{c}&=&\plug{C}{c}; c_2
\end{eqnarray*}
For this language, the only interesting case of evaluation contexts is the one that allows us to \emph{descend into the left subcommand}, because the old congruence rule invoked the step relation recursively for that position.
\newcommand{\smallstepo}[2]{#1 \to_0 #2}
The next ingredient is a reduced set of basic step rules, where we have dropped the congruence rule.
We regain the full coverage of the original rules with a new relation $\to_\mathsf{c}$, saying that we may apply $\to_0$ at the active subcommand within a larger command.
$$\infer{\smallstepc{(v, C[c])}{(v', C[c'])}}{
\smallstepo{(v, c)}{(v', c')}
}$$
Let's revisit last section's example, to see contextual semantics in action, especially to demonstrate how to express an arbitrary command as an evaluation context plugged with another command.
There exists valuation $v$ such that $\smallstepcs{(\mupd{\mempty}{\mathtt{input}}{2}, \mathtt{factorial})}{(v, \skipe)}$ and $\msel{v}{\mathtt{output}}=2$.
To showcase the convenience of contextual semantics, let's extend our example language with a simple construct for running two commands in parallel\index{parallel composition of threads}, implicitly extending the definition of plugging accordingly.
$$\begin{array}{rrcl}
\textrm{Commands}& c &::=&\ldots\mid c || c
\end{array}$$
To capture that idea that \emph{either} command in a parallel construct is allowed to step next, we extend evaluation contexts like so:
\encoding
$$\begin{array}{rrcl}
\textrm{Evaluation contexts}& C &::=&\ldots\mid C || c \mid c || C
\end{array}$$
We need one more basic step rule, to ``garbage-collect'' threads that have finished.
Our last extension with parallelism introduced intentional nondeterminism in the semantics: a single starting state can step to multiple different next states.
However, the three semantics for the original language are deterministic, and we can prove it.
\begin{theorem}
If $\bigstep{(v, c)}{v_1}$ and $\bigstep{(v, c)}{v_2}$, then $v_1= v_2$.
\end{theorem}
\begin{proof}
By induction on the derivation of $\bigstep{(v, c)}{v_1}$ and inversion on the derivation of $\bigstep{(v, c)}{v_2}$.
\end{proof}
\begin{theorem}
If $\smallstep{(v, c)}{(v_1, c_1)}$ and $\smallstep{(v, c)}{(v_2, c_2)}$, then $v_1= v_2$ and $c_1= c_2$.
\end{theorem}
\begin{proof}
By induction on the derivation of $\smallstep{(v, c)}{(v_1, c_1)}$ and inversion on the derivation of $\smallstep{(v, c)}{(v_2, c_2)}$.
\end{proof}
\begin{theorem}
If $\smallstepc{(v, c)}{(v_1, c_1)}$ and $\smallstepc{(v, c)}{(v_2, c_2)}$, then $v_1= v_2$ and $c_1= c_2$.
\end{theorem}
\begin{proof}
Follows from the last theorem and the equivalence we proved between $\to$ and $\to_\mathsf{c}$.
\end{proof}
We'll stop, for now, in our tour of useful properties of operational semantics.
All of the rest of the book is based on small-step semantics, with or without evaluation contexts.
As we study new kinds of programming languages, we will see how to model them operationally.
Almost every new proof technique is phrased as an approach to establishing invariants of transition systems based on small-step semantics.
\chapter{Abstract Interpretation and Dataflow Analysis}
The last two chapters showed us both how to build a transition system from a program automatically and how to find an invariant for a transition system automatically.
Let's now combine these ideas to find invariants for programs automatically, in a particular way associated with the technique of \emph{dataflow analysis}\index{dataflow analysis} used to drive many compiler optimizations.
Throughout, we'll stick with the example of the small imperative language whose semantics we studied in the last chapter.
We'll confine our attention to its basic small-step semantics via the $\to$ relation.
Model checking builds up increasingly larger finite sets of reachable states in a system.
A state $(v, c)$ of our imperative language combines \emph{control state}\index{control state}$c$ (the next command to execute) with \emph{data state}$v$ (the values of the variables), and so model checking will find invariants that restrict both components.
We say that model checking is \emph{path-sensitive}\index{path-sensitive analysis} because its invariants can distinguish between the different data states that can be associated with the same control state, reached along different paths in the program's executions.
Path-sensitive analyses tend to be much more computationally expensive than \emph{path-insensitive}\index{path-insensitive analysis} analyses, whose invariants collapse together all ways of reaching the same control state.
Dataflow analysis is one such path-insensitive approach, and its underlying theory is \emph{abstract interpretation}\index{abstract interpretation}.
\section{Definition of an Abstract Interpretation}
An abstract interpretation is a particular sort of abstraction, of the kind we met in studying model checking.
In that more general setting, we can represent concrete states with any sorts of abstract states.
In abstract interpretation, we most commonly associate each variable with an independent abstract description.
One example, which we'll formalize in more detail shortly, would be to label each variable as ``even,'' ``odd,'' or ``either.''
An \emph{abstract interpretation} (for our example imperative language) is a tuple $\angled{\mathbb D, \top, \mathcal C, \hat{+}, \hat{-}, \hat{\times}, \join, \sim}$, where $\mathbb D$ is a set (the domain of the analysis); $\top\in\mathbb D$; $\mathcal C : \mathbb N \to\mathbb D$; $\hat{+}, \hat{-}, \hat{\times}, \join : \mathbb D \times\mathbb D \to\mathbb D$; and $\sim\;\subseteq\mathbb N \times\mathbb D$.
\item Abstract versions of numbers are $\mathbb D$ values.
\item$\top$ (``top'')\index{top element of an abstract interpretation} is the least specific abstract value, representing any concrete value.
\item$\mathcal C$ maps any constant to its most precise abstraction.
\item$\hat{+}$, $\hat{-}$, and $\hat{\times}$ push abstraction through arithmetic operators, calculating their most precise abstractions.
\item$\join$ (``join'')\index{join operation of an abstract interpretation} computes the \emph{least upper bound}\index{least upper bound} of two abstract values: the most specific value that represents any value associated with either input.
For $a, b \in\mathbb D$, define $a \sqsubseteq b$ to mean $\forall n \in\mathbb N. \;(n \sim a)\Rightarrow(n \sim b)$. That is, $b$ is at least as general as $a$.
We generally think of an abstract interpretation as forming a \emph{lattice}\index{lattice} (actually a semilattice\index{semilattice}), which is roughly the algebraic structure characterized by operations like $\join$, when $\join$ truly returns the \emph{most specific} or \emph{least} upper bound of its two arguments. We visualize the even-odd lattice like so.
Since $\sqsubseteq$ is clearly transitive, upward-moving paths across multiple nodes also imply $\sqsubseteq$ relationships between their endpoints.
It's worth verifying quickly that any two nodes in this graph have a unique lowest common ancestor, which is the proper result of the $\join$ operation on those nodes.
Another worthwhile exercise for the reader is to work out the proper definitions of $\hat{+}$, $\hat{-}$, and $\hat{\times}$ for this domain.
\section{Flow-Insensitive Analysis}
We now give our first recipe for building a program abstraction from an abstract interpretation.
We apply a \emph{flow-insensitive} abstraction, which means we find an invariant that doesn't depend at all on the control part $c$ of a full state $(v, c)$.
Alternatively, the invariant depends only on the data part $v$.
Concretely, with $\mathbb V$ the set of variables, we work with states $s \in\mathbb V \to\mathbb D$, taking the domain $\mathbb D$ of our chosen abstract interpretation.
An abstract state $s$ for a concrete valuation $v$ assigns to each $x$ an abstract value $s(x)$ such that $v(x)\sim s(x)$.
We overload the operator $\sim$ to denote this compatibility via $v \sim s$.
\newcommand{\absexp}[1]{[#1]}
As a preliminary, we define the abstract interpretation of an expression like so:
Given command $c$, initial valuation $v$, and initial abstract state $s$ such that $v \sim s$. The transition system with initial state $s$ and step relation $\to^c_\mathsf{FI}$ simulates the system with initial state $(v, c)$ and step relation $\to$, according to a simulation relation enforcing $\sim$ between the valuation and abstract state.
\end{theorem}
Now a simple procedure can find an invariant for the abstracted system.
In particular:
\begin{enumerate}
\item Initialize $s$ with the abstract state from the theorem statement.
\item\label{flow_insensitive_loop}Compute $s' = s \join\bigsqcup_{(x, e)\in\asgns{c}}\mupd{s}{x}{\absexp{e}s}$.
\item If $s' \sqsubseteq s$, then we're done; $s$ is the invariant.
\item Otherwise, assign $s = s'$ and return to \ref{flow_insensitive_loop}.
\end{enumerate}
Every step in this outline is computable, since the abstract states will, in practice, be finite maps, where all variables not in their domains are assumed to map to $\top$.
If the outline above terminates, then it is an invariant of the flow-insensitive abstracted system that $s$ (its final value from the loop above) is an upper bound for every reachable state. That is, for every reachable $s'$, $s' \sqsubseteq s$.
\end{theorem}
To check a concrete program, we first abstract it to a flow-insensitive version with Theorem \ref{flow_insensitive_abstraction}, then we find a guaranteed invariant with Theorem \ref{flow_insensitive_iteration}.
One wrinkle here is that it is not obvious that our informal loop above always terminates.
However, it always terminates if our abstract domain has \emph{finite height}\index{finite height of abstract domain}, meaning that there is no infinite ascending chain of distinct elements $a_i$ such that $a_i \sqsubseteq a_{i+1}$ for all $i$.
Our even-odd example trivially has that property, since it contains only finitely many distinct elements.
It is worth emphasizing that, when those conditions are met, our invariant-finding procedure is guaranteed to terminate, even though the underlying language is Turing-complete, so that most interesting analysis problems are uncomputable!
The catch is that it is always possible that the invariant found is a trivial one, where the abstract state maps every variable to $\top$.
We can only go so far with flow-insensitive invariants, which don't let us record different facts about the variables for different lines of the program code.
Such an analysis will get tripped up even by straightline code where parities of variables change as we go.
The solution can be to go to \emph{flow-sensitive}\index{flow-sensitive analysis} analysis, where an abstract state $S$ is a finite map from commands to the abstract states of the previous section.
Note that the last two cases, for conditional control flow, ignore the test expression entirely, which is certainly sound, though it may lead to imprecision in the analysis.
Define $\absstepo{s}{c}$ as shorthand for $\absstep{s}{c}{\lambda c_1. \; c_1}$.
Now we can define a new abstract step relation.
$$\infer{(s, c)\to_\mathsf{FS}(s', c')}{
\absstepo{s}{c}(c') = s'
}$$
That is, we step from $(s, c)$ to $(s', c')$ precisely when, if we look up $c'$ in the result of running $c$ abstractly in $s$, we find $s'$.
Now we can follow an analogous path to the one we did in the last section.
\begin{theorem}\label{flow_sensitive_abstraction}
\abstraction
Given command $c$ and initial valuation $v$. The transition system with initial state $(s, c)$ and step relation $\to_\mathsf{FS}$ simulates the system with initial state $(v, c)$ and step relation $\to$, according to a simulation relation enforcing equality of the commands, as well as $\sim$ between the valuation and abstract state.
\end{theorem}
Now another simple procedure can find an invariant for the abstracted system.
We write $S \join S'$ for joining of two flow-sensitive abstract states.
When $c$ is in the domain of exactly one of $S$ or $S'$, $S \join S'$ agrees with the corresponding mapping.
When $c$ is in neither domain, it isn't in the domain of $S \join S'$ either.
Finally, when $c$ is in both domains, we have $(S \join S')(c)= S(c)\join S'(c)$.
Also define $S \sqsubseteq S'$ to mean that, whenever $S(c)= s$, there exists $s'$ such that $S'(c)= s'$ and $s \sqsubseteq s'$.
\item\label{flow_sensitive_loop}Compute $S' = S \join\bigsqcup_{S(c)= s}\absstepo{s}{c}$.
\item If $S' \sqsubseteq S$, then we're done; $S$ is the invariant.
\item Otherwise, assign $S = S'$ and return to \ref{flow_sensitive_loop}.
\end{enumerate}
Again, every step in this outline is computable, for the same reason as in the prior section.
\begin{theorem}\label{flow_sensitive_iteration}
\invariants
If the outline above terminates, then it is an invariant of the flow-sensitive abstracted system that, for reachable $(s, c)$, we have $S(c)= s'$ for some $s'$ with $s \sqsubseteq s'$.
\end{theorem}
Again, the last two theorems together give us a recipe for computing an invariant automatically, when the loop terminates.
The flow-sensitive procedure is guaranteed to give an invariant at least as strong as what the flow-insensitive procedure would come up with, and often it's much stronger.
Consider an abstract interpretation of \emph{intervals}\index{interval analysis}, where each elements of the domain is either $[a, b]$ or $[a, \infty)$, for $a, b \in\mathbb N$.
Restricting our attention to $a$ and $b$ values between 0 and 1 for illustration purposes, we have this diagram of the domain, where the bottom element represents an empty set.
\node(oneinf) [below right of=top] {$[1, \infty)$};
\node(zero) [below of=zeroone] {$[0, 0]$};
\node(one) [below of=oneinf] {$[1, 1]$};
\node(emp) [below right of=zero]{$[1, 0]$};
\draw(top) -- (zeroone);
\draw(top) -- (oneinf);
\draw(zeroone) -- (zero);
\draw(zeroone) -- (one);
\draw(oneinf) -- (one);
\draw(zero) -- (emp);
\draw(one) -- (emp);
\end{tikzpicture}\end{center}
The abstract operators have intuitive and simple definitions, like, flattening the different kinds of intervals into a common notation, defining $(a_1, b_1)\join(a_2, b_2)=(\min(a_1, a_2), \max(b_1, b_2))$ and $(a_1, b_1)\hat{+}(a_2, b_2)=(a_1+ a_2, b_1+ b_2)$, with usual conventions about what it means to do arithmetic with $\infty$.
Again, the lattice diagram above was simplified to cover only 0 and 1 as legal constant values.
We can define the interval lattice to draw from the full, infinite set of natural numbers.
In that case, we can quickly run into trouble with abstract interpretation.
For instance, consider this infinite-looping program:
One (flow-insensitive) invariant is that $\mathsf{a}\geq7$, represented as the abstract state $\mupd{\mempty}{\mathsf{a}}{[7, \infty)}$.
However, even the flow-sensitive analysis will keep growing the range of $\mathsf{a}$, as it traverses the loop over and over!
We see $\mathsf{a}$ initialized to $[7, 7]$, then grown to $[7, 10]$ after one loop iteration, then to $[7, 13]$ after another, and so on indefinitely.
Notice that we wrote before that termination is guaranteed when the lattice has finite height, which we have just demonstrated is not true for general intervals, as our example program generates an infinite ascending chain of distinct intervals.
\newcommand{\widen}[0]{\triangledown}
The canonical solution to this problem is to employ a \emph{widening}\index{widening} operator $\widen$.
This operator has the same soundness requirements as $\join$, but we do not require that it gives the \emph{least} upper bound of its two operands.
It merely needs to give some upper bound.
In fact, we don't want it to give least upper bounds; we want it to \emph{skip ahead} in that ordering as necessary to promote termination.
In general, we don't want to replace all uses of $\join$ with $\widen$, though it is sound to do so.
We might apply $\widen$ in place of $\join$ only for commands that are the beginnings of loops, for instance, to guarantee that no infinite path in the program avoids infinitely many encounters with $\widen$ to tame infinite ascending chains.
For intervals, when we are working with programs that we fear will keep increasing variables indefinitely through loops, a simple form of widening is defined as follows.
Set $(a_1, b_1)\widen(a_2, b_2)=(a_1, b_1)\join(a_2, b_2)$ when $b_2\leq b_1$, that is, when the upper bound of the interval hasn't increased since the last iteration.
Otherwise, set $(a_1, b_1)\widen(a_2, b_2)=(\min(a_1, a_2), \infty)$.
In other words, when an interval expands to include higher values, fast-forward its upper bound to $\infty$.
With this modification, analysis of our tricky example successfully finds the invariant $\mathsf{a}\geq7$.
In fact, flow-insensitive and flow-sensitive interval analysis with this widening operator applied at loop starts are guaranteed to terminate, for any input programs.
We'll now take a break from the imperative language we've been studying for the last two chapters, instead looking at a classic sort of small language that distills the essence of \emph{functional} programming\index{functional programming}.
That's the language paradigm that we've been using throughout this book, as we coded executable versions of algorithms.
Its distinctive characteristics are first, a computation style based on simplifying terms instead of running step-by-step instructions that modify state; and second, use of functions as first-class values.
Functional programming went mainstream in the early 21st century, influencing widely adopted languages from JavaScript\index{JavaScript}, where first-class functions are routinely used as callbacks in asynchronous event processing; to Scala\index{Scala}, a hybrid language that melds functional-programming ideas with object-oriented programming for the Java platform; to Haskell\index{Haskell}, a purely functional language that has become popular with programming hobbyists and is seeing increasing adoption in industry.
The heart of functional programming persists even in \emph{$\lambda$-calculus}\index{$\lambda$-calculus} (or lambda calculus\index{lambda calculus}), the simplest version of which contains just three syntactic forms, but which provides probably the simplest of the widely known Turing-complete languages that is (nearly!) pleasant to program in directly.
An expression $\lambda x. \; e$\index{$\lambda$ expression} is a first-class, anonymous function, also called a \emph{function abstraction}\index{function abstraction} or \emph{$\lambda$-abstraction}\index{$\lambda$-abstraction}.
When called, it replaces its formal-argument variable $x$ with the actual argument within $e$ and continues evaluating.
The third syntactic form $e \; e$ uses \emph{juxtaposition}\index{juxtaposition}, or writing one term after another, for function application.
A simple example of an expression is $\lambda x. \; x$, for an identity function.
When we apply it to itself, like $(\lambda x. \; x)\;(\lambda x. \; x)$, it reduces again to itself.
\newcommand{\fv}[1]{\textsf{FV}(#1)}
We can give a simple big-step operational semantics to $\lambda$-terms.
The key auxiliary operation is \emph{substitution}\index{substitution}, where we write $\subst{e}{x}{e'}$ for replacing all \emph{free} occurrences of $x$ in $e$ with $e'$.
Here we refer to a notion of \emph{free variables}\index{free variables}, which we should define first, as a recursive function.
\begin{eqnarray*}
\fv{x}&=&\{x\}\\
\fv{\lambda x. \; e}&=&\fv{e} - \{x\}\\
\fv{e_1 \; e_2}&=&\fv{e_1}\cup\fv{e_2}
\end{eqnarray*}
Intuitively, a variable is free in an expression iff it doesn't occur inside the scope of a $\lambda$ binding the same variable.
Next we define substitution.
\begin{eqnarray*}
\subst{x}{x}{e'}&=& e' \\
\subst{y}{x}{e'}&=& y\textrm{, if $y \neq x$}\\
\subst{\lambda x. \; e}{x}{e'}&=&\lambda x. \; e \\
\subst{\lambda y. \; e}{x}{e'}&=&\lambda y. \;\subst{e}{x}{e'}\textrm{, if $y \neq x$}\\
Notice a peculiar property of this definition when we work with \emph{open} terms\index{open terms}, whose free-variable sets are nonempty.
According to the definition $\subst{\lambda x. \; y}{y}{x}=\lambda x. \; x$.
In this example, we say that $\lambda$-bound variable $x$ has been \emph{captured}\index{variable capture} unintentionally, where substitution created a reference to that $\lambda$ where none existed before.
Such a problem can only arise when replacing a variable with an open term.
More general investigations into $\lambda$-calculus will define a more involved notion of \emph{capture-avoiding} substitution\index{capture-avoiding substitution}.
Instead, in this book, we carefully steer clear of the $\lambda$-calculus applications that require substituting open terms for variables, letting us stick with the simpler definiton.
When it comes to formal encoding of this style of syntax in proof assistants, surprisingly many complications arise, leading to what is still an active research area in encodings of language syntax with local variable binding\index{variable binding}.
Since we aim more for broad than deep coverage of the field of formal program reasoning, we are happy to avoid those complexities.
With substitution in hand, a big-step semantics\index{big-step semantics} is easy to define.
We use the syntactic shorthand $v$ for a \emph{value}\index{value}, or term that needs no further evaluation, which in this case includes just the $\lambda$-abstractions.
To evaluate an application, evaluate both the function and the argument.
The function value must be some $\lambda$-abstraction.
Substitute the argument value in the body of the abstraction, evaluate the result, and return that value as the overall value.
Note that we only ever need to evaluate \emph{closed} terms\index{closed terms}, meaning terms that are not open, so we obey the restriction on substitution sketched above.
It may be surprising that these two rules are enough to define the full semantics of a Turing-complete language!
\section{A Quick Case Study in Program Verification: Church Numerals}
\newcommand{\church}[1]{\underline{#1}}
Since $\lambda$-calculus is Turing-complete, it must be able to represent numbers and all the usual arithmetic operations.
The classic representation is \emph{Church numerals}\index{Church numerals}, where every natural number $n$ is represented as a particular $\lambda$-term $\church{n}$ that, when passed a function $f$ as input, returns $f^n$, the $n$-way self-composition of $f$.
In some sense, repeating a process is the fundamental use of a natural number, and it turns out that we can recover all of the usual operations atop this primitive.
\newcommand{\lc}[1]{\mathsf{#1}}
Two $\lambda$-calculus functions are sufficient to build up all the naturals as Church numerals.
\begin{eqnarray*}
\lc{zero}&=&\lambda f. \;\lambda x. \; x \\
\lc{plus1}&=&\lambda n. \;\lambda f. \;\lambda x. \; f \; (n \; f \; x)
\end{eqnarray*}
Our representation of 0 returns an identity function, no matter which $f$ it is passed.
Our successor operation takes in a number $n$ and returns a new one that first runs $n$ and then applies $f$ one extra time.
Now we have $\church{0}=\lc{zero}$, $\church{1}=\lc{plus1}\;\lc{zero}$, $\church{2}=\lc{plus1}\;(\lc{plus1}\;\lc{zero})$, and so on.
Let us formalize which values they evaluate to and tweak the encoding to use the values instead.
We write $\prechurch{n}$ for the body of a $\lambda$-abstraction that we are building to represent $n$, where variables $f$ and $x$ are in scope.
\begin{eqnarray*}
\prechurch{0}&=& x \\
\prechurch{n+1}&=& f \; ((\lambda f. \;\lambda x. \;\prechurch{n}) \; f \; x)
\end{eqnarray*}
The $n+1$ case may seem wastefully large, but, in fact, this is the precise form of the values produced by evaluating repeated applications of $\lc{plus1}$ to $\lc{zero}$, as the reader can verify using the big-step semantics.
We define $\church{n}=\lambda f. \;\lambda x. \;\prechurch{n}$, giving a canonical encoding for each number.
Now we notate correctness of an encoding $e$ for number $n$ by $e \sim n$, defining it as $\bigstep{e}{\church{n}}$, meaning that $e$ evaluates to the Church encoding of $n$.
Two first easy results show that our primitive constructors are correct.
\begin{theorem}
$\lc{zero}\sim0$.
\end{theorem}
\begin{theorem}
If $e_n \sim n$, then $\lc{plus1}\; e_n \sim n+1$.
\end{theorem}
Things get more interesting as we start to code up the arithmetic operations.
\begin{eqnarray*}
\lc{add}&=&\lambda n. \;\lambda m. \; n \;\lc{plus1}\; m
\end{eqnarray*}
That is, addition of $n$ to $m$ is calculated by applying $n$$\lc{plus1}$ operations to $m$.
\begin{theorem}\label{church_add}
If $e_n \sim n$ and $e_m \sim m$, then $\lc{add}\; e_n \; e_m \sim n + m$.
\end{theorem}
\begin{proof}
After a few steps applying the big-step rules directly, we finish by induction on $n$.
A silly-seeming but necessary lemma proves that $\subst{\prechurch{n}}{m}{e}=\prechurch{n}$, since $\prechurch{n}$ does not contain free occurrences of $m$.
\end{proof}
Multiplication proceeds in much the same way.
\begin{eqnarray*}
\lc{mult}&=&\lambda n. \;\lambda m. \; n \; (\lc{add}\; m) \;\lc{zero}
\end{eqnarray*}
\begin{theorem}
If $e_n \sim n$ and $e_m \sim m$, then $\lc{mult}\; e_n \; e_m \sim n \times m$.
\end{theorem}
\begin{proof}
After a few steps applying the big-step rules directly, we finish by induction on $n$, within which we appeal to Theorem \ref{church_add}.
\end{proof}
An enjoyable (though not entirely trivial) exercise for the reader is to generalize the methods of Church encoding to encoding of other inductive datatypes, including the syntax of $\lambda$-calculus itself.
A hallmark of a Turing-complete language is that it can host an interpreter for itself, and $\lambda$-calculus is no exception!
$\lambda$-calculus is also straightforward to formalize with a small-step semantics\index{small-step operational semantics} and evaluation contexts\index{evaluation contexts}, following the method of Section \ref{eval_contexts}.
One might argue that the technique is even simpler for $\lambda$-calculus, since we must deal only with expressions, not also imperative variable valuations.
$$\begin{array}{rrcl}
\textrm{Evaluation contexts}& C &::=&\Box\mid C \; e \mid v \; C
\end{array}$$
Note the one subtlety: the last form of evaluation context requires the term in a function position to be a \emph{value}.
This innocuous-looking restriction enforces \emph{call-by-value evaluation order}\index{call-by-value}, where, upon encountering a function application, we must first evaluate the function, then evaluate the argument, and only then call the function.
Tweaks to the definition of $C$ produce other evaluation orders, like \emph{call-by-name}\index{call-by-name}, but we will say no more about those alternatives.
We assume a standard definition of what it means to plug an expression into the hole in a context, and now we can give the sole small-step evaluation rule for basic $\lambda$-calculus, conventionally called the \emph{$\beta$-reduction} rule\index{$\beta$-reduction}.
That is, we find a suitable position within the expression where a $\lambda$-expression is applied to a value, and we replace that position with the appropriate substitution result.
Following a very similar outline to what we used in Chapter \ref{operational_semantics}, we establish equivalence between the two semantics for $\lambda$-calculus.
\begin{theorem}
If $\smallsteps{e}{v}$, then $\bigstep{e}{v}$.
\end{theorem}
\begin{theorem}
If $\bigstep{e}{v}$, then $\smallsteps{e}{v}$.
\end{theorem}
There are a few proof subtleties beyond what we encountered before, and the Coq formalization may be worth reading, to see those details.
Again as before, we have a natural way to build a transition system from any $\lambda$-term $e$, where $\mathcal L$ is the set of $\lambda$-terms.
We define $\mathbb T(e)=\angled{\mathcal L, \{e\}, \to}$.
The next section gives probably the most celebrated $\lambda$-calculus result based on the transition-system perspective.
Let's spruce up the language with some more constructs.
$$\begin{array}{rrcl}
\textrm{Variables}& x &\in&\mathsf{Strings}\\
\textrm{Numbers}& n &\in&\mathbb N \\
\textrm{Expressions}& e &::=& n \mid e + e \mid x \mid\lambda x. \; e \mid e \; e \\
\textrm{Values}& v &::=& n \mid\lambda x. \; e
\end{array}$$
We've added natural numbers as a primitive feature, supported via constants and addition.
Numbers may be intermixed with functions, and we may, for instance, write first-class functions that take numbers as input or return numbers.
Our language of evaluation contexts expands a bit.
$$\begin{array}{rrcl}
\textrm{Evaluation contexts}& C &::=&\Box\mid C \; e \mid v \; C \mid C + e \mid v + C
\end{array}$$
Now we want to define two kinds of basic small steps, so it is worth defining a separate relation for them.
Here we face a classic nuisance in writing rules that combine explicit syntax with standard mathematical operators, and we write $+$ for the syntactic construct and $\textbf{+}$ for the mathematical addition operator.
What would be a useful property to prove about our new expressions?
For one thing, we don't want them to ``crash,'' as in the expression $(\lambda x. \; x)+7$ that tries to add a function and a number.
No rule of the semantics knows what to do with that case, but it also isn't a value, so we shouldn't consider it as finished with evaluation.
Define an expression as \emph{stuck}\index{stuck term} when it is not a value and it cannot take a small step.
For ``reasonable'' expressions $e$, we should be able to prove that it is an invariant of $\mathbb T(e)$ that no expression is ever stuck.
To define ``reasonable,'' we formalize the popular idea of a static type system.
Every expression will be assigned a type, capturing which sorts of contexts it may legally be dropped into.
Our language of types is simple.
\abstraction
$$\begin{array}{rrcl}
\textrm{Types}&\tau&::=&\mathbb N \mid\tau\to\tau
\end{array}$$
We have trees of function-space constructors, where all the leaves are instances of the natural-number type $\mathbb N$.
Note that, with type assignment, we have yet another case of \emph{abstraction}, approximating a potentially complex expression with a type that only records enough information to rule out crashes.
\newcommand{\hasty}[3]{#1 \vdash #2 : #3}
To assign types to closed terms, we must recursively define what it means for an open term to have a type.
To that end, we use \emph{typing contexts}\index{typing context}$\Gamma$, finite maps from variables to types.
To mimic standard notation, we write $\Gamma, x : \tau$ as shorthand for $\mupd{\Gamma}{x}{\tau}$, overriding of key $x$ with value $\tau$ in $\Gamma$.
Now we define typing as a three-place relation, written $\hasty{\Gamma}{e}{\tau}$, to indicate that, assuming $\Gamma$ as an assignment of types to $e$'s free variables, we conclude that $e$ has type $\tau$.
We define the relation inductively, with one case per syntactic construct.
We write $\hasty{}{e}{\tau}$ as shorthand for $\hasty{\mempty}{e}{\tau}$, meaning that closed term $e$ has type $\tau$, with no typing context required.
Note that this style of typing rules provides another instance of \emph{modularity}, since we can separately type-check different subexpressions of a large expression, using just their types to coordinate expectations among subexpressions.
It should be an invariant of $\mathbb T(e)$ that every reachable expression has the same type as the original, so long as the original was well-typed.
This observation is the key to proving that it is also an invariant that no reachable expression is stuck, using a proof technique called \emph{the syntactic approach to type soundness}\index{syntactic approach to type soundness}, which turns out to be just another instance of our general toolbox for invariant proofs.
We work our way through a suite of standard lemmas to support that invariant proof.
\begin{lemma}[Progress]\label{progress}
If $\hasty{}{e}{\tau}$, then $e$ isn't stuck.
\end{lemma}
\begin{proof}
By induction on the derivation of $\hasty{}{e}{\tau}$.
\end{proof}
\begin{lemma}[Weakening]\label{weakening}
If $\hasty{\Gamma}{e}{\tau}$ and every mapping in $\Gamma$ is also included in $\Gamma'$, then $\hasty{\Gamma'}{e}{\tau}$.
\end{lemma}
\begin{proof}
By induction on the derivation of $\hasty{\Gamma}{e}{\tau}$.
\end{proof}
\begin{lemma}[Substitution]\label{substitution}
If $\hasty{\Gamma, x : \tau'}{e}{\tau}$ and $\hasty{}{e'}{\tau'}$, then $\hasty{\Gamma}{\subst{e}{x}{e'}}{\tau}$.
\end{lemma}
\begin{proof}
By induction on the derivation of $\hasty{\Gamma, x: \tau'}{e}{\tau}$, with appeal to Lemma \ref{weakening}.
\end{proof}
\begin{lemma}\label{preservation0}
If $\smallstepo{e}{e'}$ and $\hasty{}{e}{\tau}$, then $\hasty{}{e'}{\tau}$.
\end{lemma}
\begin{proof}
By inversion on the derivation of $\smallstepo{e}{e'}$, with appeal to Lemma \ref{substitution}.
\end{proof}
\begin{lemma}\label{generalize_plug}
If any type of $e_1$ is also a type of $e_2$, then any type of $\plug{C}{e_1}$ is also a type of $\plug{C}{e_2}$.
\end{lemma}
\begin{proof}
By induction on the structure of $C$.
\end{proof}
\begin{lemma}[Preservation]\label{preservation}
If $\smallstep{e_1}{e_2}$ and $\hasty{}{e_1}{\tau}$, then $\hasty{}{e_2}{\tau}$.
\end{lemma}
\begin{proof}
By inversion on the derivation of $\smallstep{e_1}{e_2}$, with appeal to Lemmas \ref{preservation0} and \ref{generalize_plug}.
\end{proof}
\invariants
\begin{theorem}[Type Soundness]
If $\hasty{}{e}{\tau}$, then $\neg\textrm{stuck}$ is an invariant of $\mathbb T(e)$.
\end{theorem}
\begin{proof}
First, we strengthen the invariant to $I(e)=\;\hasty{}{e}{\tau}$, justifying the implication by Lemma \ref{progress}, Progress.
Then we apply invariant induction, where the base case is trivial.
The induction step is a direct match for Lemma \ref{preservation}, Preservation.
\end{proof}
The syntactic approach to type soundness is often presented as a proof technique in isolation, but what we see here is that it follows very directly from our general invariant proof technique.
Usually syntactic type soundness is presented as fundamentally about proving Progress and Preservation conditions.
The Progress condition maps to invariant strengthening, and the Preservation condition maps to invariant induction, which we have used in almost every invariant proof so far.
Since the basic proof structure matches our standard one, the main insight is the usual one: a good choice of a strengthened invariant.
In this case, invariant $I(e)=\;\hasty{}{e}{\tau}$ is that crucial insight, including the original design of the set of types and the typing relation.
The syntactic approach to type soundness continues to apply to \emph{impure} functional languages, which combine imperative side effects with first-class functions.
We'll study the general domain through its most common exemplar: $\lambda$-calculus with \emph{mutable references}\index{mutable references}\index{references}.
The three new expression forms deal with \emph{references}, which act like, for instance, Java\index{Java} objects that only have single public fields.
We write $\newref{e}$ to allocate a new reference initialized with value $e$, we write $\readref{e}$ for reading the value stored in reference $e$, and we write $\writeref{e_1}{e_2}$ for overwriting the value of reference $e_1$ with $e_2$.
An example is worth a thousand words, so let's consider a concrete program.
In contrast to last chapter's semantics for pure $\lambda$-calculus, here we work with states that include not just expressions but also \emph{heaps}\index{heaps}$h$, partial functions from references to their current stored values.
\quad\infer{\smallstepo{(h, n + m)}{(h, n \textbf{+} m)}}{}$$
To write out the rules that are specific to references, it's helpful to extend our language syntax with a form that will never appear in original programs, but which does show up at intermediate execution steps.
In particular, let's add an expression form for \emph{locations}\index{locations}, the runtime values of references, and let's say that locations also count as values.
$$\begin{array}{rrcl}
\textrm{Locations}&\ell&\in&\mathbb N \\
\textrm{Expressions}& e &::=& n \mid e + e \mid x \mid\lambda x. \; e \mid e \; e \mid\newref{e}\mid\;\readref{e}\mid\writeref{e}{e}\mid\underline{\ell}\\
\textrm{Values}& v &::=& n \mid\lambda x. \; e \mid\underline{\ell}
\end{array}$$
\newcommand{\dom}[1]{\mathsf{dom}(#1)}
Now we can write the rules for the three reference primitives.
To evaluate a reference allocation $\newref{e}$, we nondeterministically\index{nondeterminism} pick some unused location $\ell$ and initialize it with the requested value.
To read from a reference in $\readref{e}$, we just look up the location in the heap; the program will be \emph{stuck} if the location is not already included in $h$.
Finally, to write to a reference with $\writeref{e_1}{e_2}$, we check that the requested location is already in the heap (we're stuck if not), then we overwrite its value with the new one.
Here is the overall step rule, which looks just like the one for basic $\lambda$-calculus, with a heap wrapped around everything.
As a small exercise for the reader, it may be worth using this judgment to derive that our example program from before always returns 1.
Even fixing the empty heap in the starting state, there is some nondeterminism in which final heap it returns: the possibilities are all the single-location heaps, mapping their single locations to value 1.
It is natural to allow this nondeterminism in allocation, since typical memory allocators in real systems don't give promises about predictability in the addresses that they return.
However, we will be able to prove that, for instance, any program returning a number \emph{gives the same answer, independently of nondeterministic choices made by the allocator}.
That property is not true in programming languages like C\index{C programming language} that are not \emph{memory safe}\index{memory safety}, as they allow arithmetic and comparisons on pointers\index{pointers}, the closest C equivalent of our references.
For $\lambda$-calculus with references, we can prove a similar type-soundness theorem to what we proved last chapter, though the proof has a twist or two.
To start with, we should define our extended type system, with one new case for references.
$$\begin{array}{rrcl}
\textrm{Types}&\tau&::=&\mathbb N \mid\tau\to\tau\mid\underline{\reft{\tau}}
\end{array}$$
Here are the rules from last chapter's basic $\lambda$-calculus, which we can keep unchanged.
That's enough notation to let us state type soundness, which is indeed provable.
\begin{theorem}[Type Soundness]
If $\hasty{}{e}{\tau}$, then $\neg\textrm{stuck}$ is an invariant of $\mathbb T(e)$.
\end{theorem}
However, we will need to develop some more machinery to let us state the strengthened invariant that makes the proof go through.
\newcommand{\rhasty}[4]{#1; #2 \vdash #3 : #4}
The trouble with our typing rules is that they disallow location constants, but those constants \emph{will} arise in intermediate states of program execution.
To prepare for them, we introduce \emph{heap typings}\index{heap typings}$\Sigma$, partial functions from locations to types.
The idea is that a heap typing $\Sigma$ models a heap $h$ by giving the intended type for each of its locations.
We define an expanded typing judgment of the form $\rhasty{\Sigma}{\Gamma}{e}{\tau}$, with a new parameter included solely to enable the following rule.
We have made some progress toward stating an inductive invariant for the type-soundness theorem.
The essential idea of the proof is found in the invariant choice $I(h, e)=\exists\Sigma. \;\rhasty{\Sigma}{\mempty}{e}{\tau}$.
However, we can tell that something is suspicious with this invariant, since it does not mention $h$.
We should also somehow characterize the relationship between $\Sigma$ and $h$.
\newcommand{\heapty}[2]{#1 \vdash #2}
Here is a first cut at defining a relation $\heapty{\Sigma}{h}$.
$$\infer{\heapty{\Sigma}{h}}{
\forall\ell, \tau. \;\msel{\Sigma}{\ell} = \tau\Rightarrow\exists v. \;\msel{h}{\ell} = v \land\rhasty{\Sigma}{\mempty}{v}{\tau}
}$$
In other words, whenever $\Sigma$ announces the existence of location $\ell$ meant to store values of type $\tau$, the heap $h$ actually stores some value $v$ for $\ell$, and that value has the right type.
Note the tricky recursion inherent in typing $v$ with respect to the very same $\Sigma$.
This rule as stated is not \emph{quite} sufficient to make the invariant inductive.
We could get stuck on a $\newref{e}$ expression if the heap $h$ becomes \emph{infinite}, with no free addresses left to allocate.
Of course, we know that finite executions, started in the empty heap, only produce finite intermediate heaps.
Let's remember that fact with another condition in the $\heapty{\Sigma}{h}$ relation.
$$\infer{\heapty{\Sigma}{h}}{
(\forall\ell, \tau. \;\msel{\Sigma}{\ell} = \tau\Rightarrow\exists v. \;\msel{h}{\ell} = v \land\rhasty{\Sigma}{\mempty}{v}{\tau})
We prove variants of all of the lemmas behind last chapter's type-safety proof, with a few new ones and twists on the originals.
Here we give some highlights.
\begin{lemma}[Heap Weakening]
If $\rhasty{\Sigma}{\Gamma}{e}{\tau}$ and every mapping in $\Sigma$ is also included in $\Sigma'$, then $\rhasty{\Sigma'}{\Gamma}{e}{\tau}$.
\end{lemma}
\begin{lemma}\label{preservation0}
If $\smallstepo{(h, e)}{(h', e')}$, $\rhasty{\Sigma}{\mempty}{e}{\tau}$, and $\heapty{\Sigma}{h}$, then there exists $\Sigma'$ such that $\rhasty{\Sigma'}{\mempty}{e'}{\tau}$, $\heapty{\Sigma'}{h'}$, and $\Sigma'$ preserves all mappings from $\Sigma$.
\end{lemma}
\begin{lemma}\label{generalize_plug}
If $\rhasty{\Sigma}{\mempty}{\plug{C}{e_1}}{\tau}$, then there exists $\tau_0$ such that $\rhasty{\Sigma}{\mempty}{e_1}{\tau_0}$ and, for all $e_2$ and $\Sigma'$, if $\rhasty{\Sigma'}{\mempty}{e_2}{\tau_0}$ and $\Sigma'$ preserves mappings from $\Sigma$, then $\rhasty{\Sigma'}{\mempty}{\plug{C}{e_2}}{\tau}$.
\end{lemma}
\begin{lemma}[Preservation]\label{preservation}
If $\smallstep{(h, e)}{(h', e')}$, $\rhasty{\Sigma}{\mempty}{e}{\tau}$, and $\heapty{\Sigma}{h}$, then there exists $\Sigma'$ such that $\rhasty{\Sigma'}{\mempty}{e'}{\tau}$ and $\heapty{\Sigma'}{h'}$.
Functional languages like ML\index{ML} and Haskell\index{Haskell} include features very similar to the mutable references that we study in this chapter.
However, their execution models depart in an important way from the operational semantics we just defined: they use \emph{garbage collection}\index{garbage collection} to deallocate unused references, whereas our last semantics allows references to accumulate forever in the heap, even if it is clear that some of them will never be needed again.
Worry not!
We can model garbage collection with one new rule of the operational semantics, and then our type-safety proof adapts and shows that we still avoid stuckness, when the garbage collector can snatch \emph{unreachable} locations away from us at any moment.
\newcommand{\freeloc}[1]{\mathsf{freeloc}(#1)}
To define \emph{unreachable}, we start with a way to compute the \emph{free locations} of an expression.
In order, the rules say: any location reaches itself; any location reaches anywhere reachable from the value assigned to it by $h$; and any expression reaches anywhere reachable from any of its free locations.
The reason has to do with our formulation of type safety, by saying that programs never get \emph{stuck}.
We defined that $e$ is \emph{stuck} if it is not a value, but it also can't take a step.
If we omitted from the garbage-collection rule the premise $h' \neq h$, then this rule would \emph{always} apply, for any term, simply by setting $h' = h$.
That is, \emph{no} term would ever be stuck, and type safety would be meaningless!
Since the rule also requires that $h'$ be \emph{no larger than}$h$ (with the second premise), additionally requiring $h' \neq h$ forces $h'$ to \emph{shrink}, garbage-collecting at least one location.
Thus, in any execution state, we can ``kill time'' by running garbage collection only finitely many times before we need to find some ``real'' step to run.
More precisely, the limit on how many times we can run garbage collection in a row, starting from heap $h$, is $|\dom{h}|$, the number of locations in $h$.
The type-safety proof is fairly straightforward to update.
We prove progress by \emph{ignoring} the garbage-collection rule, since the existing rule was already enough to find a step for every nonvalue.
A bit more work is needed to update the proof of preservation; its case for the existing rule follows the same way as before, while we must prove a few lemmas on the way to handling the new rule.
\begin{lemma}[Transitivity for reachability]
If $\freeloc{e_1}\subseteq\freeloc{e_2}$, then $\reach{h}{e_1}\subseteq\reach{h}{e_2}$.
\end{lemma}
\begin{lemma}[Irrelevance of unreachable locations for typing]
If $\heapty{\Sigma}{h}$, $\rhasty{\Sigma}{\Gamma}{e}{\tau}$, then $\rhasty{\Sigma'}{\Gamma}{e}{\tau}$, if we also know that, for all $\ell$ and $\tau'$, when $\ell\in\reach{h}{e}$ and $\msel{\Sigma}{\ell}=\tau'$, it follows that $\msel{\Sigma'}{\ell}=\tau'$.
\end{lemma}
\begin{lemma}[Reachability sandwich]
If $\ell\in\reach{h}{e}$, $\msel{h}{\ell}= v$, and $\ell' \in\reach{h}{v}$, then $\ell' \in\reach{h}{e}$.
\end{lemma}
To extend the proof of preservation, we need to show that the strengthened invariant still holds after garbage collection.
A key element is choosing the new heap typing.
We pick \emph{the restriction of the old heap typing $\Sigma$ to the domain of the new heap $h'$}.
That is, we drop from the heap typing all locations that have been garbage collected, preserving the types of the survivors.
Some work is required to show that this strategy is sound, given the definition of reachability, but the lemmas above work out the details, leaving just a bit of bookkeeping in the preservation proof.
The final safety proof then proceeds in exactly the same way as before.
Our proof here hasn't quite covered all the varieties of garbage collectors that exist.
In particular, \emph{copying collectors}\index{copying garbage collectors} may \emph{move references to different locations}, while we only allow collectors to delete some references.
It may be an edifying exercise for the reader to extend our proof in a way that also supports reference relocation.
We now take a step away from the last chapters in two dimensions: we switch back from functional to imperative programs, and we return to proofs of deep correctness properties, rather than mere absence of type-related crashes.
Nontheless, the essential proof structure winds up being the same, as we once again prove invariants of transition systems!
To provide us with an interesting enough playground for program verification, let's begin by defining an imperative language with an infinite mutable heap.
For reasons that will become clear shortly, we do a strange bit of mixing of syntax and semantics.
In certain parts of the syntax, we include \emph{assertions}\index{assertions}$a$, which are arbitrary mathematical predicates over program state, split between heaps $h$ and variable valuations $v$.
$$\begin{array}{rrcl}
\textrm{Numbers}& n &\in&\mathbb N \\
\textrm{Variables}& x &\in&\mathsf{Strings}\\
\textrm{Expressions}& e &::=& n \mid x \mid e + e \mid e - e \mid e \times e \mid\readfrom{e}\\
\textrm{Boolean expressions}& b &::=& e = e \mid e < e \\
\textrm{Commands}& c &::=&\skipe\mid\assign{x}{e}\mid\writeto{e}{e}\mid c; c \\
Beside assertions, we also have memory-read operations $\readfrom{e}$ and memory-write operations $\writeto{e_1}{e_2}$, which are written suggestively, as if the memory were a global array named $*$.
Loops have sprouted an extra assertion in their syntax, which we will actually ignore in the language semantics, but which becomes important as part of the proof technique we will learn, especially in automating it.
Much as we did with type systems, we define a syntactic predicate and prove it sound once and for all.
Afterward, we can automatically show that particular programs and their specifications inhabit the predicate.
This time, predicate instances will be written like $\hoare{P}{c}{Q}$, with $c$ the command being verified, $P$ its \emph{precondition}\index{precondition} (assumption about the program state before we start running $c$), and $Q$ its \emph{postcondition} (obligation about the program state after $c$ finishes).
We call any such fact a \emph{Hoare triple}\index{Hoare triple}, and the overall predicate is an instance of \emph{Hoare logic}\index{Hoare logic}.
\encoding
A first rule for $\skipe$ is easy: anything that was true before is also true after.
$$\infer{\hoare{P}{\skipe}{P}}{}$$
A rule for assignment is slightly more involved: to state what we know is true after, we recall that there existed a prestate satisfying the precondition, which then evolved into the poststate in the expected way.
$$\infer{\hoare{P}{\assign{x}{e}}{\lambda(h, v). \;\exists v'. \; P(h, v')\land v =\mupd{v'}{x}{\denote{e}(h, v')}}}{}$$
The memory-write command is treated symmetrically.
To model sequencing, we thread predicates through in an intuitive way.
$$\infer{\hoare{P}{c_1; c_2}{R}}{
\hoare{P}{c_1}{Q}
&\hoare{Q}{c_2}{R}
}$$
For conditional statements, we start from the basic approach of sequencing, adding two twists.
First, since the two subcommands run after different outcomes of the test expression, we extend their preconditions.
Second, since we may reach the end of the command after running either subcommand, we take the disjunction of their postconditions.
$$\infer{\hoare{P}{\ifte{b}{c_1}{c_2}}{\lambda s. \; Q_1(s)\lor Q_2(s)}}{
\hoare{\lambda s. \; P(s) \land\denote{b}(s)}{c_1}{Q_1}
&\hoare{\lambda s. \; P(s) \land\neg\denote{b}(s)}{c_2}{Q_2}
}$$
Coming to loops, we at least have a purpose for the assertion annotated on each one.
We call those assertions \emph{loop invariants}\index{loop invariants}; one of these is meant to be true every time a loop iteration begins.
We will try to avoid confusion with the more fundamental concept of invariant for transition systems, though in fact the two are closely related formally, which we will see in the last section of this chapter.
Essentially, the loop invariant gives the \emph{induction hypothesis} that makes the program correctness proof go through.
We encapsulate the induction reasoning once and for all, in the proof of soundness for Hoare triples.
To verify an individual program, it is only necessary to prove the premises of the rule, which we give now.
$$\infer{\hoare{P}{\{I\}\while{b}{c}}{\lambda s. \; I(s)\land\neg\denote{b}(s)}}{
(\forall s. \; P(s) \Rightarrow I(s))
&\hoare{\lambda s. \; I(s) \land\denote{b}(s)}{c}{I}
}$$
In words: the loop invariant is true when we begin the loop, and every iteration preserves the invariant, given the extra knowledge that the loop test succeeded.
If the loop finishes, we know that the invariant is still true, but now the test is false.
The final command-specific rule, for assertions, is a bit anticlimactic.
The precondition is carried over as postcondition, if it is strong enough to prove the assertion.
$$\infer{\hoare{P}{\assert{I}}{P}}{
\forall s. \; P(s) \Rightarrow I(s)
}$$
One more essential rule remains, this time not specific to any command form.
The rules we've given deduce specific kinds of precondition-postcondition pairs.
For instance, the $\skipe$ rule forces the precondition and postcondition to match.
However, we expect to be able to prove $\hoare{\lambda(h, v). \;\msel{v}{x} > 0}{\skipe}{\lambda(h, v). \;\msel{v}{x}\geq0}$, because the postcondition is \emph{weaker}\index{weaker predicate} than the precondition, meaning the precondition implies the postcondition.
Alternatively, the precondition is \emph{stronger}\index{stronger predicate} than the postcondition, because the precondition keeps all restrictions from the postcondition while adding new ones.
Hoare Logic's \emph{rule of consequence}\index{rule of consequence} allows us to build a new Hoare triple from an old one by \emph{strengthening the precondition}\index{strengthening the precondition} and \emph{weakening the postcondition}\index{weakening the postcondition}.
$$\infer{\hoare{P'}{c}{Q'}}{
\hoare{P}{c}{Q}
& (\forall s. \; P'(s) \Rightarrow P(s))
& (\forall s. \; Q(s) \Rightarrow Q'(s))
}$$
These rules together are \emph{complete}\index{completeness of Hoare logic}, in the sense that any intuitively correct precondition-postcondition pair for a command is provable.
Here we only go into detail on a proof of the dual property, \emph{soundness}\index{soundness of Hoare logic}.
\begin{lemma}\label{hoare_while}
Assume the following fact: Together, $\bigstep{(h, v, c)}{(h', v')}$, $I(h, v)$, and $\denote{b}(h, s)$ imply $I(h', v')$.
Then, given $\bigstep{(h, v, \{I\}\while{b}{c})}{(h', v')}$, it follows that $I(h', v')$ and $\neg\denote{b}(h', v')$.
\end{lemma}
\begin{proof}
By induction on the derivation of $\bigstep{(h, v, \{I\}\while{b}{c})}{(h', v')}$.
\end{proof}
That lemma encapsulates once and for all the use of induction in reasoning about the many iterations of loops.
\begin{theorem}[Soundness of Hoare logic]
If $\hoare{P}{c}{Q}$, $\bigstep{(h, v, c)}{(h', v')}$, and $P(h, v)$, then $Q(h', v')$.
\end{theorem}
\begin{proof}
By induction on the derivation of $\hoare{P}{c}{Q}$ and inversion on the derivation of $\bigstep{(h, v, c)}{(h', v')}$, appealing to Lemma \ref{hoare_while} in the appropriate case.
\end{proof}
We leave concrete example derivations to the accompanying Coq code, as that level of fiddly detail deserves to be machine-checked.
Note that there is a rather effective automated proof procedure lurking behind the rules introduced in this section:
To prove a Hoare triple, first try applying the rule associated with its top-level syntax-tree constructor (e.g., assignment or loop rule).
If the conclusion of that rule does unify with the goal, apply the rule and proceed recursively on its premises.
Otherwise, apply the rule of consequence to replace the postcondition with one matching that from the matching rule; note that all rules accept arbitrarily shaped preconditions, so we don't actually need to do work to massage the precondition.
After a step like this one, it is guaranteed that the ``fundamental'' rule now applies.
This process creates a pile of side conditions to be proved by other means, corresponding to the assertion implications generated by the rules for loops, assertions, and consequence.
Many real-world tools based on Hoare logic discharge such goals using solvers for satisfiability modulo theories\index{satisfiability modulo theories}, otherwise known as SMT solvers\index{SMT solvers}.
The accompanying Coq code just uses a modest Coq automation tactic definition building on the proof steps we have been using all along.
It is not complete by any means, but it does surprisingly well in the examples we step through, of low to moderate complexity.
Before closing our discussion of the basics of Hoare logic, let's consider how it brings to bear some more of the general principles that we have met before.
\abstraction
A command's precondition and postcondition serve as an \emph{abstraction} of the command: it is safe to model a command with its specification, if it has been proved using a Hoare triple.
\modularity
Furthermore, the Hoare rules themselves take advantage of \emph{modularity} to analyze subcommands separately, mediating between them using only the specifications.
The implementation details of a subcommand don't matter for any other subcommands in the program, so long as that subcommand has been connected to a specification that preserves enough information about its behavior.
It is an art to choose the right specification for each piece of a program.
Detailed specifications minimize the chance that some other part of the program winds up unprovable, despite its correctness, but more detailed specifications also tend to be harder to prove in the first place.
Last section's soundness theorem only lets us draw conclusions about programs that terminate.
We call such guarantees \emph{partial correctness}\index{partial correctness}.
Other forms of Hoare triples guarantee \emph{total correctness}\index{total correctness}, which includes termination.
However, sometimes programs aren't meant to terminate, yet we still want to gain confidence about their behavior.
To that end, we first give a small-step semantics for the same programming language.
Then we prove a different soundness theorem for the same Hoare-triple predicate, showing that it also implies a useful invariant for programs as transition systems.
The small-step relation is quite similar to the one from last chapter, though now our states are triples $(h, v, c)$, of heap $h$, variable valuation $v$, and command $c$.
Coq\index{Coq} is a proof-assistant software package developed as open source, primarily by Inria\index{Inria}, the French national computer-science lab.
\section{Installation and Basic Use}
The project home page is:
\begin{center}
\url{https://coq.inria.fr/}
\end{center}
The code associated with this book is designed to work with Coq versions 8.4 and higher.
The project Web site makes a number of versions available, and versions are also available in popular OS package distributions, along with binaries for platforms where open-source package systems are less common.
We assume that readers have installed Coq by one of those means or another.
It will also be almost essential to use some graphical interface for Coq editing.
The author prefers Proof General\index{Proof General}, an Emacs\index{Emacs} mode:
\begin{center}
\url{http://proofgeneral.inf.ed.ac.uk/}
\end{center}
It should be possible to follow along using CoqIDE\index{CoqIDE}, a standalone tool distributed with Coq itself, but we will not give any CoqIDE-specific instructions.
The Proof General instructions are simple: after installing, within a regular Emacs session, open a file with the Coq extension \texttt{.v}.
Move the point (cursor) to a position where you would like to examine the current state of a proof, etc.
Then press C-C C-RET (``control-C, control-enter'') to run Coq up to that point.
Several display panes will open, showing different aspects of Coq's state, any error messages it wants to report, etc.
This feature is the main workhorse of Proof General.
It can be used both to move \emph{forward}, checking that Coq accepts a command; and to move \emph{backward}, to undo commands processed previously.
Proof General has plenty of other bells and whistles, but we won't go into them here.
\section{Tactic Reference}
\emph{Tactics} are the commands run in Coq to advance the state of a proof, corresponding to deduction steps at different granularities.
Here we collect all of the short explanations of tactics that appear in Coq source files associated with the chapters included in this document.
Note that many of these are specific to the \texttt{Frap} library distributed with this book, where built-in tactics often do quite similar things, but in a way that the author judges to be more of a hassle for beginners.
\begin{description}
\item[\texttt{apply} $H$] For $H$ a hypothesis or previously proved theorem, establishing some fact that matches the structure of the current conclusion, switch to proving $H$'s own hypotheses. This is \emph{backwards reasoning} via a known fact.
\item[\texttt{apply} $H$ \texttt{with} \texttt{(}$x_1$\texttt{ := }$e_1$\texttt{) ... (}$x_n$\texttt{ := }$e_n$\texttt{)}] Like the last one, supplying values for quantified variables in $H$'s statement, especially for those variables whose values aren't immediately implied by the current goal.
\item[\texttt{apply} $H_1$ \texttt{in} $H_2$] Like \texttt{apply}$H_1$, but used in a \emph{forward} direction rather than \emph{backward}. For instance, if $H_1$ proves $P \Rightarrow Q$ and $H_2$ proves $P$, then the effect is to change $H_2$ to $Q$.
\item[\texttt{assert} $P$] First prove proposition $P$, then continue with it as a new hypothesis.
\item[\texttt{assumption}] Prove a conclusion that matches a hypothesis exactly.
\item[\texttt{cases} $e$] Break the proof into one case for each constructor that might have been used to build the value of expression $e$. In the special case where $e$ essentially has a Boolean type, we consider whether $e$ is true or false.
\item[\texttt{constructor}] When proving an instance of an inductive predicate, \texttt{apply} the first matching rule of that predicate.
\item[\texttt{eapply} $H$] Like \texttt{apply} but will work even when some quantified variables from $H$ do not have their values determined immediately by the form of the goal. Instead, \emph{existential variables} (with names starting with question marks) are introduced for those values.
\item[\texttt{eassumption}] Like \texttt{assumption} but will figure out values of existential variables.
\item[\texttt{econstructor}] When proving an instance of an inductive predicate, \texttt{eapply} the first matching rule of that predicate.
\item[\texttt{equality}] A complete decision procedure for the theory of equality and uninterpreted functions. That is, the goal must follow from only reflexivity, symmetry, transitivity, and congruence of equality, including that functions really do behave as functions. See Section \ref{decidable}.
\item[\texttt{exfalso}] From any proof state, switch to proving \texttt{False}. In other words, indicate a switch to a proof by contradiction.
\item[\texttt{exists} $e$] Prove $\exists x. \; P(x)$ by proving $P(e)$.
\item[\texttt{first\_order}] Simplify a goal into zero or more new goals, based on the rules of first-order logic alone. \emph{Warning:} this tactic is especially likely to run forever, on complex enough goals! (While entailment for propositional logic is decidable, entailment for first-order logic isn't.)
\item[\texttt{f\_equal}] When the goal is an equality between two applications of the same function, switch to proving that the function arguments are pairwise equal.
\item[\texttt{induct} $x$] Where $x$ is a variable in the theorem statement, structure the proof by induction on the structure of $x$. You will get one generated subgoal per constructor in the inductive definition of $x$. (Indeed, it is required that $x$'s type was introduced with \texttt{Inductive}.)
\item[\texttt{invert} $H$] Replace hypothesis $H$ with other facts that can be deduced from the structure of $H$'s statement. More detail to be added here soon!
\item[\texttt{linear\_arithmetic}] A complete decision procedure for linear arithmetic. Relevant formulas are essentially those built up from variables and constant natural numbers and integers using only addition and subtraction, with equality and inequality comparisons on top. (Multiplication by constants is supported, as a shorthand for repeated addition.) See Section \ref{decidable}.
\item[\texttt{rewrite} $H$] Where $H$ is a hypothesis or previously proved theorem, establishing \texttt{forall x1 .. xN, e1 = e2}, find a subterm of the goal that equals \texttt{e1}, given the right choices of \texttt{xi} values, and replace that subterm with \texttt{e2}.
\item[\texttt{rewrite} $H_1$ \texttt{in} $H_2$] Like \texttt{rewrite}$H_1$ but performs the rewrite in hypothesis $H_2$ instead of in the conclusion.
\item[\texttt{right}] Prove a disjunction by proving its right side.
\item[\texttt{ring}] Prove goals that are equalities over some registered ring or semiring, in the sense of algebra, where the goal follows solely from the axioms of that algebraic structure. See Section \ref{decidable}.
\item[\texttt{simplify}] Simplify throughout the goal, applying the definitions of recursive functions directly. That is, when a subterm matches one of the \texttt{match} cases in a defining \texttt{Fixpoint}, replace with the body of that case, then repeat.
\item[\texttt{trivial}] Coq maintains a database of simple proof steps, such as proving a fact by direct appeal to a matching hypothesis. \texttt{trivial} asks to try all such simple steps.
For more Coq information, we recommend a few books (beyond the Coq reference manual). Some focus purely on introducing Coq:
\begin{itemize}
\item Adam Chlipala, \emph{Certified Programming with Dependent Types}, MIT Press, \url{http://adam.chlipala.net/cpdt/}
\item Yves Bertot and Pierre Cast\'eran, \emph{Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions}, Springer, \url{https://www.labri.fr/perso/casteran/CoqArt/}
\end{itemize}
The first of these two, especially, goes in-depth on the automated proof-scripting principles showcased from time to time in the Coq example code associated with the present book.
There are also other sources that introduce program-reasoning principles at the same time, including:
\begin{itemize}
\item Benjamin C. Pierce et al., \emph{Software Foundations}, \url{http://www.cis.upenn.edu/~bcpierce/sf/}
\end{itemize}
\emph{Software Foundations} generally proceeds at a slower pace than this book does.
