ACF : Analyse et Conception Formelles
"Software Formal Analysis and Design"
First year of Master
in Computer Science
, Université de Rennes 1
What is it about?
course is about using formal methods to design verified software components. To
tackle this goal we rely on functional programming, first
order logic for specifying properties, proof assistant for
property checking on programs and the Scala programming
language for integrating the verified components into a
Java application. With regards to verification, we study
and use the powerful proof
tactics and counter-example finders embedded
in the Isabelle/HOL proof assistant. For code generation,
we use the awesome Scala code exportation feature of
functional programming, first order logic, formal
specification and formal verification;
2020 (and no other version) proof assistant and
counter-example finders (see a short
introduction) and the programming language.
students' final achievement is a verified Scala component
achieving price negociation in a web application. The
component is designed and verified in Isabelle/HOL. Then,
the functional code is exported to Scala and integrated in
the Java (web) application.
Disclaimer: this is a
course on formal software design and not on proof design.
Students are given a limited set of proof tactics that is
enough to prove properties defined during the lab
sessions. However, resulting proofs can be long and
cumbersome. As a result, it is accepted that properties
are not proven but only checked using Isabelle/HOL
powerful counter-example finders.
with forums etc. (Rennes 1 students only!)
consists of 7 lectures and 11 lab sessions. Lecture notes (cm1.pdf
to cm7.pdf) are (almost) in english, the lab notes (tp0.pdf to
tp8-10.pdf) are in french. The Isabelle/HOL survival
gives an idea of the used subset of Isabelle commands. Lectures
contains exercises that were solved on Isabelle/HOL by students on
my computer (and projected) during the lecture.
The course schedule is the following:
- tp0.pdf : teasing... a simple Java lab session ... to
show that designing a (simple) software can be very error prone.
It is nearly impossible to directly come up with the correct
program for this (refined) simple list inclusion test, either in
imperative or in recursive style. The objective is to motivate
the fact that defining the expected properties is crucial to
detect problems and, in the end, be sure that the solution is
correct. An (opaque) Java oracle
is given to the students to test their code and know how far
their program is from the solution. An overall of 5% students
ended up with the correct program within 2 hours.
- intro.pdf : overall objectives and
organization of the course.
- cm1.pdf : propositional and first order
logic, interpretations and models in Isabelle/HOL
- cm2.pdf, initial theory for the
course cm2.thy : terms, functions, lambda-calculs
and types (export_code to Scala).
- tp1.pdf, initial theory for the lab
session tp1.thy : first lab on
Isabelle/HOL: propositional and first order logic
(auto+nitpick). There are some additional exercises for those
who wants to know more about proof techniques in Isabelle/HOL: tp1bis.thy.
- cm3.pdf, initial theory for the
course cm3.thy : recursive functions (fun,
- cm4.pdf Video
initial theory for the
course cm4.thy : basic proof tactics
(auto, induct, sledgehammer, nitpick, quickcheck). The more
advanced topics of this course are presented in this other video (in french) with
the pc.thy Isabelle/HOL file. Students
interested by a deeper presentation of the proof assistant can
have a look to the Isabelle/HOL tutorial in the short Isabelle/HOL bibliography.
- tp2.pdf : (lab sessions 2 and 3):
recursive functions and basic proof tactics. Defining and
proving usual boolean operations on sets implemented as lists in
this (empty) theory file. We do the
same for a basic implementation of tables.
We also provide an other exercise which is a simple theory file in which the 4 main
lemmas admit counterexamples. Some of the lemmas need some fine
tuning of Nitpick and Quickcheck for the counterexamples to be
found: this is the purpose of this exercise.
- cm5.pdf Scala Crash Course. Video
(in french). We
start from the following Scala
Basics of Scala, functional programming in Scala, object model,
case classes, pattern-matching and interoperability with Java.
Deeper informations on the language are available from
M. Odersky, L. Spoon and B. Venners online book
and from those selected documents.
- tp4.pdf : lab on Scala.
Implementation of an evaluator and a pretty printer for a simple
imperative language... using pattern matching to avoid using the
visitor design pattern. We start from the following project.
- cm6.pdf, initial theory for the
course cm6.thy : certified programming and
existing certified programming chains.
- tp5.pdf, TP5_ACF.zip
: development of a glob
simplifier. A glob is a unix pattern accepting a set of (file)
names, e.g., *.txt that accepts all file names ending by '.txt'.
Simpliying a glob means to produce a glob that is smaller (or
equal) and accepts the same set of words. This first simplifier
is programmed directly in Scala.
- tp5bis.pdf, TP5bis_ACF.zip, tp5bis.thy (Available as soon as TP5
has been finished): they redo the glob
simplifier but in Isabelle/HOL and prove its correction: the
simplifier should (at least) produce a glob accepting the same
set of words. In the end, simplifiers of TP5 and TP5bis are
uploaded on the web and attacked by all students.
- cm7.pdf, initial theory for the
course cm7.thy : software
- tp67.pdf, tp67.thy,
TP67_ACF.zip : they design a
static analyser for a simple toy language, define the
correctness theorem to guarantee the safety of the analyzer,
define the completeness theorem to refine it (using the
counterexamples). Integrated with a Scala parser for the toy
language. To carry out the
proofs you can get inspiration from this short video (in french) with
the pc.thy Isabelle/HOL file.
- tp8-10.pdf, tp8-10.thy,
TP89_ACF.zip, table.thy: they design a validation
tool for a price negociation web application. A merchant and a
client send messages to the validation tool to negociate a
price. A price is validated if a price proposed by a client is
superior or equal to a price proposed by the merchant. In the
end, the list of validated should be correct. As with all
protocols, more complex than it seems at first glance. They
define the functions, check the 8 properties and export the
Scala code. All the validations tools of all students are then
deployed on a web site so that all students can attack all
validation tools and report on the attacks found. To carry out the proofs you
can get inspiration from this short video (in french) with
the pc.thy Isabelle/HOL file. For this
lab session a list of relevant intermediate lemmas (in french)
is also provided: tp8-10proof.thy.
Tools for Lab sessions
- We use Isabelle/HOL
2020 (and no other version). See the installation
Then, if you plan to
use Isabelle/HOL for all
lab sessions, you will have to install and configure a few
- To have a full quickcheck (with narrowing): install the Gnu
Haskell Compiler and in the file $ISABELLE_HOME/etc/settings,
set the ISABELLE_GHC variable to the path where the binaries
of the compile (i.e. the command ghc) is installed
Olivier Barais, Erwan Bousse , Benoît Combemalle,
Khalil Ghorbal, Manuel Leduc, Julien Richard-Foy, Sophie Pinchinat
, and Pierre Wilke
to people of the Isabelle/HOL team at TUM: Tobias Nipkow, Jasmin
Blanchette, Lukas Bulwahn, Florian Haftmann and Alexander Krauss
answering questions and for fruitful discussions.
Many thanks to Olivier Barais, Sandrine Blazy, Benoît Combemale,
Jobin, Julien Richard-Foy and Gweltaz Riou for their help during
the preparation of this course.