First
year of Master
in Computer Science at ISTIC,
Université de Rennes 1

Instructor: Thomas Genet

Teaching Assistants (2015-2016): BenoĆ®t Combemale, Sophie Pinchinat and Pierre Wilke

Teaching Assistants (2015-2016): BenoĆ®t Combemale, Sophie Pinchinat and Pierre Wilke

- Subjects: functional
programming, first order logic, formal specification and formal
verification;

- Tools: Isabelle/HOL (2014) proof assistant and counter-example finders and the programming language.

This 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 Isabelle/HOL.

The 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. Thus, students are given a limited set of proof tactics that is not sufficient to prove complex properties. As a result, properties of last lab sessions are generally not proven but only checked using Isabelle/HOL powerful counter-example finders.

The course 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 kit 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. Students are also given a small (well as focused as possible on the course objective) bibliography on Isabelle/HOL.

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
(auto+nitpick).

- 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).
Plus additional exercises for those who are familiar with sequent
calculus: tp1bis.thy and Defs.thy

- cm3.pdf, initial theory for the course cm3.thy : recursive functions (fun, function, primrec).
- cm4.pdf, initial
theory for the course cm4.thy : basic proof tactics (auto,
induct, sledgehammer,
nitpick, quickcheck). Students
interested by a deeper presentation of the proof assistant can
have a look at the Isabelle/HOL tutorial in
the short Isabelle/HOL bibliography.
We also provide two Isabelle/HOL files LOG.thy
and Defs.thy if you are interested in using
standard natural
deduction rules in Isabelle/HOL. Those who are more familiar
with sequent
calculus should get by, by replacing introduction/elimination by
the adapted left/right annotation :-).

- tp2.pdf : (lab sessions 2 and 3):
recursive functions and basic proof tactics. Defining and proving usual
boolean operations on sets implemented as lists. 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. 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.
Implement
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 Eclipse
project. Integrate the (certified) implementation of set
operations (done in lab sessions 2 and 3) to perform automated testing of other (bugged)
implementations, available in this eclipse project.

- cm6.pdf, initial
theory for the course cm6.thy
: certified programming and
existing certified programming
chains.

- tp5.pdf, TP5ACF.zip, tp5.thy
: they redo tp0.pdf but with
Isabelle/HOL and Scala code export. They use the same Java oracle to
test their
solution. An overall of 50% students ended up with the correct program
within 2 hours.

- cm7.pdf, initial
theory for the course cm7.thy
: software verification techniques.

- tp67.pdf, tp67.thy,
TP67ACF.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.

- tp8-10.pdf, tp8-10.thy, TP8-10ACF.zip : 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.

- We use Isabelle/HOL 2014. See the installation instruction first! Then, if you plan to use Isabelle/HOL for all lab sessions, you will have to install and configure a few things:
- 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
- To use Z3 with sledgehammer, set the Isabelle system option "z3_non_commercial" to "yes" (e.g. via the Isabelle/jEdit menu Plugin Options / Isabelle / General).
- To have a full sledgehammer under linux: install libwww

- ScalaIDE, or an eclipse 4.4
(Luna) with Scala 2.11 pluggin to be compatible with the course material we provide.

Many thanks to Olivier Barais, Sandrine Blazy, Benoît Combemale, Arnaud Jobin, Julien Richard-Foy and Gweltaz Riou for their help during the preparation of this course.