Written by Luka Kerr on November 30, 2020
Introduction
Theorem Provers
A theorem prover is the implementation of a formal logic on a computer. It can be:
 fully automated (propositional logic)
 automated, but not necessarily terminating (first order logic)
 with automation, but mainly interactive (higher order logic)
It also:
 is based on rules and axioms
 can deliver proofs
Theorem proving allows us to analyse systems and programs thoroughly, find design and specification errors early and give assurance that programs are correct.
This course will use Isabelle – a generic interactive proof assistant. This means it is:
 generic: not specialised to one particular logic
 interactive: more than just yes/no, you can interactively guide the system
 a proof assistant: helps to explore, find, and maintain proofs
Although, just because you prove something on a computer, does not make it necessarily correct. This is because:
 hardware could be faulty
 operating system could be faulty
 implementation runtime system could be faulty
 compiler could be faulty
 …
Meta Logic
The meta logic is a logic used to formalize another logic. Isabelle has a meta logic, specifically:
 $\bigwedge \ \equiv \ \forall$, the universal quantifier
 $\Longrightarrow \ \equiv \ \longrightarrow$, implication
$\lambda$Calculus
The $\lambda$calculus was created by Alonzo Church. It was originally meant as foundation of mathematics, is important applications in theoretical computer science and is the foundation of computability and functional programming.
Untyped $\lambda$Calculus
The untyped $\lambda$calculus is a turing complete model of computation that provides a simple way of writing down functions.
For example, instead of writing f(x) = x + 5
, we write $f = \lambda x. \ x + 5$ which is a term and a nameless function that adds 5 to its parameter.
Function Application
To apply arguments to functions, we write $f \ a$, for example $(\lambda x. \ x + 5) \ a$. To evaluate this term, we replace $x$ by $a$.
Formal Specification
Formally, the untyped lambda calculus can be defined as:
\[\begin{array}{lclr} t & ::= & v \  \ c \  \ (t \ t) \  \ (\lambda x. \ t) & (\text{terms}) \\ v, x & \in & V & (\text{variables}) \\ c & \in & C & (\text{constants}) \\ \end{array}\]Conventions
 Leave out parentheses where possible
 List variables instead of multiple $\lambda$
Rules
 Application binds to the left: $x \ y \ z = (x \ y) \ z \ne x \ (y \ z)$
 Abstraction binds to the right: $\lambda x. \ x \ y = \lambda x. \ (x \ y) \ne (\lambda x. \ x) \ y$
$\beta$reduction
The process of $\beta$reduction is simply to continuously replace the parameter by argument until you reach a point where you cannot anymore, known as the normal form.
$\beta$conversion is defined as $s =_\beta t$ iff $\exists n. s \longrightarrow_\beta^\ast n \land t \longrightarrow_\beta^\ast n$, where $\longrightarrow_\beta^\ast$ is the transitive, reflexive closure of $\longrightarrow_\beta$.
A term $t$ is reducible if there is an $s$ such that $t \longrightarrow_\beta s$.
$\eta$conversion
 $(\lambda x. \ t \ x) \longrightarrow_\eta t$ if $x \not\in FV(t)$
 $s \longrightarrow_\eta s^\prime \Longrightarrow (s \ t) \longrightarrow_\eta (s^\prime \ t)$
 $t \longrightarrow_\eta t^\prime \Longrightarrow (s \ t) \longrightarrow_\eta (s \ t^\prime)$
 $s \longrightarrow_\eta s^\prime \Longrightarrow (\lambda x. \ s) \longrightarrow_\eta (\lambda x. \ s^\prime)$
$s =_\eta t$ iff $\exists n. s \longrightarrow_\eta^\ast n \land t \longrightarrow_\eta^\ast n$, where $\longrightarrow_\beta^\ast$ is the transitive, reflexive closure of $\longrightarrow_\beta$.
Free Variables
In $(\lambda x. \ t)$, $x$ is a bound variable.
The free variables of a term are:
 $FV \ \{ x \} = \{ x \}$
 $FV \ \{ c \} = \{ \}$
 $FV \ \{ s \ t \} = FV(s) \cup FV(t)$
 $FV \ \{ \lambda x. \ t \} = FV(t) \setminus \{ x \}$
A term $t$ is called closed if $FV(t) = \{ \}$.
Substitution
When substituting, if there are name collisions we simply rename bound variables.
 $x [ x \gets t ] = t$
 $y [ x \gets t ] = y$ if $x \ne y$
 $c [ x \gets t ] = c$
 $(s_1 \ s_2) [ x \gets t ] = (s_1 [x \gets t] \ s_2 [x \gets t])$
 $(\lambda x. \ s) [x \gets t] = (\lambda x. \ s)$
 $(\lambda x. \ s) [x \gets t] = (\lambda x. \ s[x \gets t])$ if $x \ne y$ and $y \not\in FV(t)$
 $(\lambda x. \ s) [x \gets t] = (\lambda x. \ s[y \gets z][x \gets t])$ if $x \ne y$ and $z \not\in FV(t) \cup FV(s)$
$\alpha$conversion
$s =_\alpha t$ means $s = t$ up to renaming of bound variables.
Formally:
 $(\lambda x. \ t) \longrightarrow_\alpha (\lambda y. \ t[x \gets y])$ if $y \not\in FV(t)$
 $s \longrightarrow_\alpha s^\prime \Longrightarrow (s \ t) \longrightarrow_\alpha (s^\prime \ t)$
 $t \longrightarrow_\alpha t^\prime \Longrightarrow (s \ t) \longrightarrow_\alpha (s \ t^\prime)$
 $s \longrightarrow_\alpha s^\prime \Longrightarrow (\lambda x. \ s) \longrightarrow_\alpha (\lambda x. \ s^\prime)$
Also, $s =_\alpha t$ iff $s \longrightarrow_\alpha^\ast t$, where $\longrightarrow_\alpha^\ast$ is the transitive, reflexive closure of $\longrightarrow_\alpha$.
Typed $\lambda$Calculus
Terms:
\[\begin{array}{lclr} t & ::= & v \  \ c \  \ (t \ t) \  \ (\lambda x. \ t) & (\text{terms}) \\ v, x & \in & V & (\text{variables}) \\ c & \in & C & (\text{constants}) \\ \end{array}\]Types:
\[\begin{array}{lclr} \tau & ::= & b \  \ v \  \ \tau \Rightarrow \tau & (\text{types}) \\ b & \in & \{ \texttt{bool}, \texttt{int}, \dots \} & (\text{base types}) \\ v & \in & \{ \alpha, \beta, \dots \} & (\text{type variables}) \\ \end{array}\]Context $\Gamma$: a function from variable and constant names to types.
A term $t$ has a type $\tau$ in context $\Gamma$: $\Gamma \vdash t :: \tau$. Such a term is well typed if there are $\Gamma$ and $\tau$ such that $\Gamma \vdash t :: \tau$ holds.
Type Checking Rules
Variables
$\dfrac{}{\Gamma \vdash x :: \Gamma(x)}$
Application
$\dfrac{\Gamma \vdash t_1 :: \tau_2 \Rightarrow \tau \quad \Gamma \vdash t_2 :: \tau_2}{\Gamma \vdash (t_1 \ t_2) :: \tau}$
Abstraction
$\dfrac{\Gamma[x \gets \tau_x] \vdash t :: \tau}{\Gamma \vdash (\lambda x. \ t) :: \tau_x \Rightarrow \tau}$
Most General Types
Each type correct term has a most general type. We have
\[\Gamma \vdash t :: \tau \Longrightarrow \exists \sigma . \Gamma \vdash t :: \sigma \land (\forall \sigma^\prime. \Gamma \vdash t :: \sigma^\prime \Longrightarrow \sigma^\prime \lesssim \sigma)\]Subject Reduction
Well typed terms stay well typed during $\beta$reduction:
\[\Gamma \vdash s :: \tau \land s \longrightarrow_\beta t \Longrightarrow \Gamma \vdash t :: \tau\]Natural Deduction
Rules
\[\begin{array}{ccc} \rule[4ex]{0pt}{10ex} \dfrac{A \quad B}{A \land B} \texttt{conjI} & \dfrac{A}{A \lor B} \texttt{disjI1} & \dfrac{B}{A \lor B} \texttt{disjI2} \\ \rule[4ex]{0pt}{10ex} \dfrac{A \land B \quad \llbracket A; B \rrbracket \implies C}{C} \texttt{conjE} & \dfrac{A \implies B}{A \longrightarrow B} \texttt{impI} & \dfrac{A \implies False}{\neg A} \texttt{notI} \\ \rule[4ex]{0pt}{10ex} \dfrac{A \lor B \quad A \implies C \quad B \implies C}{C} \texttt{disjE} & \dfrac{A \longrightarrow B \quad A \quad B \implies C}{C} \texttt{impE} & \dfrac{\neg A \quad A}{P} \texttt{notE} \\ \rule[4ex]{0pt}{10ex} \dfrac{A \implies B \quad B \implies A}{A = B} \texttt{iffI} & \dfrac{A = B}{A \implies B} \texttt{iffD1} & \dfrac{A = B}{B \implies A} \texttt{iffD2} \\ \rule[4ex]{0pt}{10ex} \dfrac{A = B \quad \llbracket A \longrightarrow B; B \longrightarrow A \rrbracket \implies C}{C} \texttt{iffE} & \dfrac{}{True} \texttt{TrueI} & \dfrac{False}{P} \texttt{FalseE} \\ \rule[4ex]{0pt}{10ex} \dfrac{}{t = t} \texttt{refl} & \dfrac{s = t}{t = s} \texttt{sym} & \dfrac{r = s \quad s = t}{r = t} \texttt{trans} \\ \rule[4ex]{0pt}{10ex} \dfrac{s = t \quad P \ s}{P \ t} \texttt{subst} & \dfrac{\neg A \implies False}{A} \texttt{ccontr} & \dfrac{\neg A \implies A}{A} \texttt{classical} \\ \rule[4ex]{0pt}{10ex} \dfrac{}{P = True \lor P = False} \texttt{TorF} & \dfrac{}{P \log \neg P} \texttt{excludedmiddle} & \dfrac{\bigwedge x. \ P \ x}{\forall x. \ P \ x} \texttt{allI} \\ \rule[4ex]{0pt}{10ex} \dfrac{\forall x. \ P \ x \quad P \ ?x \implies R}{R} \texttt{allE} & \dfrac{\exists x. \ P \ x \quad \bigwedge x. \ P \ x \implies R}{R} \texttt{exE} & \dfrac{P \ ?x}{\exists x. \ P \ x} \texttt{exI} \\ \rule[4ex]{0pt}{10ex} \dfrac{P \land Q}{P} \texttt{conjunct1} & \dfrac{P \land Q}{Q} \texttt{conjunct2} & \dfrac{P \longrightarrow Q \quad P}{Q} \texttt{mp} \\ \rule[4ex]{0pt}{10ex} \dfrac{\forall x. \ P \ x}{P \ ?x} \texttt{spec} & & \end{array}\]Safe & Unsafe Rules
Safe rules preserve provability: conjI
, impI
, notI
, iffI
, refl
, ccontr
, classical
, conjE
, disjE
, allI
, exE
.
Unsafe rules can turn a provable goal into an unprovable one: disjI1
, disjI2
, impE
, iffD1
, iffD2
, notE
, allE
, exI
.
Safe rules should always be applied before unsafe ones.
Higher Order Logic
 Quantification over everything, including predicates
 Consistency by types
 Formula = term of type bool
 Definition built on $\lambda^\to$ with certain default types and constants
Default Types:
 $\texttt{bool}$
 $\_ \Rightarrow \_$
 $\texttt{ind}$
Default Constants:
 $\longrightarrow :: \texttt{bool} \Rightarrow \texttt{bool} \Rightarrow \texttt{bool}$
 $= :: \alpha \Rightarrow \alpha \Rightarrow \texttt{bool}$
 $\epsilon :: (\alpha \Rightarrow \texttt{bool}) \Rightarrow \alpha$
Definitions:
 $\texttt{True} \equiv (\lambda x :: \texttt{bool}. \ x) = (\lambda x. \ x)$
 $\texttt{All} \ P \equiv P = (\lambda x . \ \texttt{True})$
 $\texttt{Ex} \ P \equiv \forall Q. (\forall x. \ P \ x \longrightarrow Q) \longrightarrow Q$
 $\texttt{False} \equiv \forall P . \ P$
 $\neg P \equiv P \longrightarrow \texttt{False}$
 $P \land Q \equiv \forall R. \ (P \longrightarrow Q \longrightarrow R) \longrightarrow R$
 $P \lor Q \equiv \forall R. \ (P \longrightarrow R) \longrightarrow (Q \longrightarrow R) \longrightarrow R$
 $\texttt{If} \ P \ x \ y \equiv \texttt{SOME} \ z. \ (P = \texttt{True} \longrightarrow z = x) \land (P = \texttt{False} \longrightarrow z = y)$
 $\texttt{inj} \ f \equiv \forall x \ y. \ f \ x = f \ y \longrightarrow x = y$
 $\texttt{surj} \ f \equiv \forall y. \ \exists x. \ y = f \ x$
Axioms:
\[\begin{array}{ccc} \rule[4ex]{0pt}{10ex} \dfrac{}{P = True \lor P = False} \texttt{TorF} & \dfrac{}{t = t} \texttt{refl} & \dfrac{s = t \quad P \ s}{P \ t} \texttt{subst} \\ \rule[4ex]{0pt}{10ex} \dfrac{}{(P \longrightarrow Q) \longrightarrow (Q \longrightarrow P) \longrightarrow (P = Q)} \texttt{iff} & \dfrac{P \longrightarrow Q \quad P}{Q} \texttt{mp} & \dfrac{P \implies Q}{P \longrightarrow Q} \texttt{impI} \\ \rule[4ex]{0pt}{10ex} \dfrac{}{\exists f :: \texttt{ind} \Rightarrow \texttt{ind}. \ \text{inj} \ f \land \neg \text{surj} \ f} \texttt{infty} & \dfrac{\bigwedge x. \ f \ x = g \ x}{(\lambda x. \ f \ x) = (\lambda x. \ g \ x)} \texttt{ext} & \dfrac{P \ ?x}{P (\texttt{SOME} \ x. \ P \ x)} \texttt{someI} \end{array}\]Isar
A typical Isar proof looks like:
proof
assume formula0
have formula1 by simp
...
have formulan by blast
show formula(n + 1) by ...
qed
which proves formula0
implies formula(n + 1)
.
proof
proof <method> <statement>* qed
proof <method>
: applies method to the stated goalproof
applies a single rule that fitsproof 
does nothing to the goal
Modes
[prove]
 goal has been stated, proof needs to follow
[state]
 proof block has opened or subgoal has been proved, new
from
statement, goal statement or assumptions can follow
 proof block has opened or subgoal has been proved, new
[chain]
from
statement has been made, goal statement needs to follow
Backward & Forward
 Backward reasoning:
have A /\ B proof
proof
picks an intro rule automatically conclusion of rule must unify with
A /\ B
 Forward reasoning:
assume AB: "A /\ B"; from AB have "..." proof
 now
proof
picks an elimination rule automatically  trigger by
from
 first assumption of rule must unify with
AB
 now
General case: from A1 ... An have R proof
 first
n
assumptions of rule must unify withA1 ... An
 conclusion of rule must unify with
R
Fix & Obtain
fix v1 ... vn
 introduces new arbitrary but fixed variables
obtain v1 ... vn where <prop> <proof
 introduces new variables together with property
Abbreviations
this
: the previous fact proved or assumedthen
:from this
thus
:then show
hence
:then have
with A1 ... An
:from A1 ... An this
?thesis
: the last enclosing goal statement
Moreover & Ultimately
moreover have Pn
instead ofhave Xn: Pn
Term Rewriting
Given a set of equations $l_1 = r_1$, $l_2 = r_2$, …, $l_n = r_n$, does equation $l = r$ hold?
The idea of term rewriting is to use equations as reduction rules, i.e. $l_1 \longrightarrow r_1$, $l_2 \longrightarrow r_2$, …, $l_n \longrightarrow r_n$ to help decide whether $l = r$ by deciding $l \overset{\ast}{\longleftrightarrow} r$.
Arrow Definitions
 $\overset{0}{\longrightarrow} \ = \{ (x, \ y) \mid x = y \}$: identity
 $\overset{n + 1}{\longrightarrow} \ = \ \overset{n}{\longrightarrow} \circ \longrightarrow$: $n + 1$ fold composition
 $\overset{+}{\longrightarrow} \ = \bigcup_{i > 0} \overset{i}{\longrightarrow}$: transitive closure
 $\overset{\ast}{\longrightarrow} \ = \ \overset{+}{\longrightarrow} \cup \overset{0}{\longrightarrow}$: reflexive transitive closure
 $\overset{=}{\longrightarrow} \ = \ \longrightarrow \cup \overset{0}{\longrightarrow}$: reflexive closure
 $\overset{1}{\longrightarrow} \ = \{ (y, \ x) \mid x \longrightarrow y \}$: inverse
 $\longleftarrow \ = \ \overset{1}{\longrightarrow}$: inverse
 $\longleftrightarrow \ = \ \longleftarrow \cup \longrightarrow$: symmetric closure

$\overset{+}{\longleftrightarrow} \ = \bigcup_{i > 0} \overset{i}{\longleftrightarrow}$: symmetric closure
 $\overset{\ast}{\longrightarrow} \ = \ \overset{+}{\longleftrightarrow} \cup \overset{0}{\longleftrightarrow}$: reflexive transitive symmetric closure
Deciding $l \overset{\ast}{\longleftrightarrow} r$
To decide whether $l \overset{\ast}{\longleftrightarrow} r$ holds, we look for an $n$ such that $l \overset{\ast}{\longrightarrow} n$ and $r \overset{\ast}{\longrightarrow} n$.
Although, there may not be a suitable $n$. This decision only works for systems where the ChurchRosser property holds:
\[l \overset{\ast}{\longleftrightarrow} r \implies \exists n. \ l \overset{\ast}{\longrightarrow} n \land r \overset{\ast}{\longrightarrow} n\]Confluence
If terms in a system can be rewritten in more than one way to yield the same result, then the system is confluent.
Termination
 $\longrightarrow$ is terminating if there are no infinite reduction chains
 $\longrightarrow$ is normalising if each element has a normal form
 $\longrightarrow$ is convergent if it is both terminating and confluent
When each rule application makes terms simpler in some way, then $\longrightarrow$ is terminating. More formally, $\longrightarrow$ is terminating when there is a well founded order $<$ on terms for which $s < t$ whenever $t \longrightarrow s$. An order is well founded if there is no infinite decreasing chains $a_1 > a_2 > \dots$.
In practice, it is often easier to consider just the rewrite rules by themselves, rather than their application to an arbitrary term $t$. To do this, we show for each rule $l_i = r_i$, that $r_i < l_i$. This requires a term $u$ to become smaller whenever any subterm of $u$ is made smaller. Formally, this means that $<$ is required to be monotonic with respect to the structure of terms: $s < t \longrightarrow u[s] < u[t]$. This is true for most orders that don’t treat certain parts of terms as special cases.
Term Rewriting In Isabelle
The term rewriting engine in Isabelle is called the simplifier. To use it, we write apply simp
. The simplifier uses simplification rules and applies them from left to right until no rule is applicable. Both termination and confluence is not guaranteed.
Equations can be turned into simplication rules by adding the [simp]
attribute, or they can be added/deleted locally using apply (simp add: <rules>)
or apply (simp del: <rules>)
. Certain rules can be applied alone using apply (simp only: <rules>)
.
Applying A Rewrite Rule
A rule $l \longrightarrow r$ is applicable to a term $t[s]$ if there is a substitution $\sigma$ such that $\sigma \ l = s$. The resulting term is $t[\sigma \ r]$, and we have $t[s] = t[\sigma \ r]$.
Conditional Term Rewriting
Rewrite rules can be conditional, where $\llbracket P_1, \dots, P_n \rrbracket \implies l = r$ is applicable to a term $t[s]$ with $\sigma$ if $\sigma \ l = s$ and $\sigma \ P_1, \dots, \sigma \ P_n$ are provable by rewriting.
Rewriting With Assumptions
Isabelle uses assumptions in rewriting, this can lead to nontermination. There are options we can pass to simp
to disable this:
(simp (no_asm))
: use and simplify assumptions(simp (no_asm_use))
: ignore assumptions(simp (no_asm_simp))
: use, but do not simplify assumptions
Orthogonal Rewriting Systems
 A rule $l \longrightarrow r$ is leftlinear if no variable occurs twice in $l$
 A rewrite system is leftlinear if all rules are
A system is orthogonal if it is leftlinear and has no critical pairs. Orthogonal rewrite systems are confluent.
Specification Techniques
Sets
Type 'a set
sets over type 'a
.
{}
,{a, b, c, d}
,{x. P x}
 $e \in A$, $A \subseteq B$
 $A \cup B$, $A \cap B$, $A  B$, $A$
 $\bigcup x \in A. \ B \ x$, $\bigcap x \in A. \ B \ x$, $\bigcap A$, $\bigcup A$
 $\{ i .. j \}$
insert :: 'a => 'a set => 'a set
 … and so on
Introducing Theorems
 Definitions
definition x where "..."
introduces a new lemma calledx_def
 Proofs
lemma "..."
Introducing Types
typedecl
: by name onlytypedecl names
introduces a new typenames
without any further assumptions
type synonym
: by abbreviationtype_synonym 'a rel = "'a => 'a => bool"
introduces abbreviationrel
for existing type
typedef
: by definition as a settypedef new_type = "{ some set }" <proof>
introduces a new type as a subset of an existing type the proof shows that the set on the right hand side is nonempty
Inductive Definitions
The rules
\[\dfrac{a_1 \in X \quad \dots \quad a_n \in X}{a \in X} \ \text{with} \ a_1, \dots, a_n, a \in A\]define a set $X \subseteq A$.
Given a set of rules $R \subseteq A \ \text{set} \times A$, we can apply $R$ to a set $B$: $\hat{R} \ B \equiv \{ x . \ \exists H. \ (H, x) \in R \land H \subseteq B \}$.
The set $B$ is $R$closed iff $\hat{R} \ B \subseteq B$, and $X$ is the least $R$closed subset of A.
Rule Induction
\[\dfrac{\forall(\{ a_1, \dots, a_n \}, a) \in R. \ P \ a_1 \land \dots \land P \ a_n \implies P \ a}{\forall x \in X. \ P \ x}\]Datatypes
\[\begin{array}{lcl} \mathbf{datatype} \ (\alpha_1, \dots, \alpha_n) \ \tau & = & C_1 \ \tau_{1,1} \dots \tau_{1,n_1} \\ &  & \dots \\ &  & C_k \ \tau_{k,1} \dots \tau_{k,n_k} \end{array}\]Datatypes must be definable as a set, and can’t have nested recursion.
Every datatype introduces a case
construct, where in general there is one case per constructor. The syntax apply (case_tac t)
creates $k$ subgoals, one for each constructor.
Recursion
In HOL, all functions must be total. Primitive recursion functions in Isabelle guarantee termination structurally. A primitive recursive function can be introduced with primrec
.
Induction
Structural Induction
$P \ xs$ holds for all lists $xs$ if
 $P \ Nil$
 and for arbitrary $x$ and $xs$, $P \ xs \implies P \ (x \sharp xs)$
A general proof method for induction is (induct x)
, where x
must be a free variable in the first subgoal, and the type of x
must be a datatype.
Theorems about recursive functions are proved by induction.
fun
Defining a recursive function using fun
allows for high expressiveness, but a termination proof may fail. In genera, fun
is
 more permissive than
primrec
 generates more theorems than
primrec
 may fail to prove termination
Each fun
definition induces an induction principle. For each equation, show $P$ holds for the left hand side, provided $P$ holds for each recursive call on the right hand size.
Isabelle tries to prove termination automatically, which works in most cases but may fail. In this case, termination can be proved seperately.
Automation
Sledgehammer
 Connects Isabelle with ATPs and SMT solvers: E, SPASS, Vampire, CVC3, Yices, Z3
 Simple to invocate
 users don’t need to select or know facts
 or ensure the problem is firstorder
 or know anything about the automated prover
 Exploits local parallelism and remote servers
Reconstruction
We don’t want to trust the external provers. Need to check/reconstruct proof.
 Refind using Metis: usually fast and reliable (sometimes too slow)
 Rerun external prover for trusted replay: used for SMT, reruns prover each time
 Recheck stored explicit external representation of proof: used for SMT, no need to rerun, fragile
 Recast into structured Isar proof: fast, not always readable
Disproof
Testing cannot prove theorems, but it can refute conjectures. Usage with quickcheck
Quickcheck
Lightweight validation by testing.
 Motivated by Haskell’s QuickCheck
 Uses Isabelle’s code generator
 Fast
 Runs in background, proves you wrong as you type
Covers a number of testing approaches:
 Random and exhausing testing
 Smart test data generators
 Narrowingbased (symbolic) testing
Nitpick
Finite model finder based on SAT. Soundly approximates infinite types. Usage with nitpick
.
Hoare Logic
The idea of Hoare Logic is to describe the meaning of program by pre/post conditions. Together, a program with these pre and post conditions is known as a Hoare Triple:
\[\{ P \} \quad C \quad \{ Q \}\]To prove properties about programs, we have rules that directly work on such triples.
Partial correctness: $\models \{ P \} \ C \ \{ Q \} \equiv \forall \sigma \ \sigma^\prime. \ P \ \sigma \land \langle c, \sigma \rangle \to \sigma^\prime \longrightarrow Q \ \sigma^\prime$.
Total correctness: $\models \{ P \} \ C \ \{ Q \} \equiv (\forall \sigma \ \sigma^\prime. \ P \ \sigma \land \langle c, \sigma \rangle \to \sigma^\prime \longrightarrow Q \ \sigma^\prime) \land (\forall \sigma. \ P \ \sigma \longrightarrow \exists \sigma^\prime. \ \langle c, \sigma \rangle \to \sigma^\prime)$
Soundness: $\vdash \{ P \} \ C \ \{ Q \} \implies \models \{ P \} \ C \ \{ Q \}$.
Soundness can be proved by rule induction on $\vdash \{ P \} \ C \ \{ Q \}$.
Invariants
For programs with loops, we need to find a correct invariant $P$, with which we annotate the program with so that Hoare rules can be applied automatically.
Weakest Preconditions
\[\mathbf{pre} \ C \ Q = \mathbf{weakest} \ P \ \mathbf{such \ that} \ \{ P \} \ C \ \{ Q \}\]Verification Conditions
The triple $\{ \mathbf{pre} \ C \ Q \} \ C \ \{ Q \}$ is only true under certain conditions, called verification conditions $vc \ C \ Q$. We also have $vc \ C \ Q \land (P \implies \mathbf{pre} \ C \ Q) \implies \{ P \} \ C \ \{ Q \}$.
Proofs About Programs
Deep Embeddings
A deep embedding is a seperate representation of language terms and their semantics.
This allows for proof of general theorems about the language, not just of programs, usually by structural induction over the syntax type.
A disadvantage is that semantically equivalent programs are not obviously equal, and many concepts already present in the logic must be reinvented.
Shallow Embeddings
A shallow embedding represents only the semantics, directly in the logic. It includes a definition for each language construct, giving its semantics. Programs are represented as instances of these definitions.
A shallow embedding is suitable for (a useful fragment of) C.
State Monad
The state monad can express lots of C ideas:
 Access to volatile variables, external APIs: Nondeterminism
 Undefined behaviour: Failure
 Early exit (
return
,break
,continue
): Exceptional control flow
A tool called AutoCorres produces a verified translation from deeply embedded C to a monadic representation specifically designed for humans to do proofs over.
The state monad models the semantics of a deterministic computation as a function: $s \Rightarrow (\alpha \times s)$. The computation operates over a state of type $s$ which includes all global variables, external devices etc. The computation also yields a return value of type $\alpha$ which models exit statuses, return values etc.
A function return
is provided that represents the computation that leaves the state unchanged and returns its argument: $\texttt{return} \ x \equiv \lambda s. \ (x, s)$.
Basic Operations
get
($\texttt{get} \equiv \lambda s. \ (s, s)$): returns the entire state without modifying itput
($\texttt{put} \equiv \lambda _. \ ((), s)$): replaces the state and returns the unit value $()$bind
($\texttt{c »= d} \equiv \lambda s. \ \mathbf{let} \ (r, s^\prime) = c \ s \ \mathbf{in} \ d \ r \ s^\prime$): sequences two computations; 2nd takes the first’s resultgets
($\texttt{gets f} \equiv \texttt{get »=} \ (\lambda s. \ \texttt{return} \ (f s))$): returns a projection of the state; leaves state unchangedmodify
($\texttt{modify f} \equiv \texttt{get »=} \ (\lambda s. \ \texttt{put} \ (f s))$): applies its argument to modify the state; returns $()$
Laws
Formally, a monad $M$ is a type constructor with two operations: $\texttt{return} :: \alpha \Rightarrow M \ \alpha$ and $\texttt{bind} :: M \ \alpha \Rightarrow (\alpha \Rightarrow M \ \beta) \Rightarrow M \ \beta$.
Also, a >>= b
is infix notation for bind a b
, and a >>= (\x. b x)
is often written as do { x < a; b x }
.
The laws are:
 returnleft:
(return x >>= f) = f x
 returnright:
(m >>= return) = m
 bindassoc:
((a >>= b) >>= c) = (a >>= (\x. b x >>= c))
State Monad With Failure
$s \Rightarrow ((\alpha \times s) \times \texttt{bool})$
Nondeterministic State Monad With Failure
$s \Rightarrow ((\alpha \times s) \ \texttt{set} \times \texttt{bool})$
Where computations return a set of possible results.
C Verification
wp
The syntax apply (wp <extrawprules>)
is a tactic for automatic application of weakest precondition rules. When used with AutoCorres, it allows for automated reasoning about C programs.
AutoCorres
AutoCorres reduces the pain in reasoning about C code. It is selfcertifying, in that it produces Isabelle theorems proving its own correctness.
Word Abstraction
Word abstraction converts a C integer into an Isabelle integer, and a C unsigned into an Isabelle natural number. Guards are inserted to ensure absence of unsigned underflow and overflow.
Isabelle
General Schema
lemma name: "<goal>"
apply <method>
apply <method>
...
done
Sequential application of methods until all subgoals are solved.
Theories
theory MyTh
import ImpThy1 ... ImpThyn
begin
...
end
 MyTh is name of theory, and must live in
MyTh.thy
 ImpThyi is the name of imported theories
 Usually,
theory MyTh imports Main begin ... end
will suffice
Rules
apply assumption
: proves $\llbracket B_1; \dots; B_m \rrbracket \implies C$ by unifying $C$ with one of $B_i$
Intro Rules
Decompose formulae to the right of $\implies$.
apply (rule <introrule>)
 Applying rule $\llbracket A_1; \dots; A_n \rrbracket \implies A$ to subgoal $C$:
 unifies $A$ and $C$
 replaces $C$ with $n$ new subgoals $A_1, \dots A_n$
Elimination Rules
Decompose formulae on the left of $\implies$.
apply (erule <elimrule>)
 Applying rule $\llbracket A_1; \dots; A_n \rrbracket \implies A$ means if $A_1$ is known and $A$ wants to be proven, it suffices to show $A_2, \dots A_n$
 Applying rule $\llbracket A_1; \dots; A_n \rrbracket \implies A$ to subgoal $C$:
 Like
rule
but also unifies first premise of rule with an assumption and eliminates that assumption
 Like
Cases
apply (case_tac <term>)
: case distinctions on arbitrary terms
Instantiating Rules
apply (rule_tac x=<term> in <rule>)
orapply (erule_tac x=<term> in <rule>)
. Like
rule
, but?x
in<rule>
is instantiated by<term>
before application.
Renaming Parameters
(rename tac x1 ... xn)
: renames the rightmost (inner)n
parameters tox1 ... xn
Forward Proofs
apply (frule <rule>)
: used when the first premise of theorem matches a premise of the current goalapply (drule <rule>)
: like frule except it deletes the matching premise
Automation
apply (intro <introrules>)
: repeatedly applies intro rulesapply (intro <elimrules>)
: repeatedly applies elimination rulesapply safe
: applies all safe rulesapply clarify
: applies all safe rules that do not split the goalapply blast
: an automatic tableaux prover that works on firstorder logicapply auto
: applies automated tools to look for solutionapply fast
: another automatic search tacticapply force
: like auto, but only for the first goalapply fastforce
: a combination of fast and forceapply simp
: simplifies current goal using term rewritingapply (simp add <theorems>)
: like the simplifier, but tells the simplifier to use additional theorems as wellapply clarsimp
: a combination of clarify and simpapply arith
: automatically solves linear arithmetic problems