A short Introduction to Isabelle
French-Italian Summer School of Computer Science
Collegno, August 28, 2006
Teacher:Stefano Berardi (
http://www.di.unito.it/~stefano/ ), e-mail: stefano.berardi address:
Course Notes: All
files of the course
, including: slides in .ppt, the solution of Hotel Key Cards exercise, a 16 hour course on Isabelle, more exercices and more solutions (2Mb). Alternatively, only
slides in pdf
Aim of the Course:
The Kepler Conjecture says that the "cannonball packing" is a densest packing of 3-dimensional balls of the same size. This was stated as a fact by Kepler in 1611 but only proved by Thomas Hales in 1998. His proof relies on a Java program for generating all (3000) possible counterexamples (all of which are then shown not to be counterexamples). Isabelle group was able to prove the correctness of a functional implementation of his Java program.
The Java Bytecode Verifier (JBV) is an essential part of the Java security architecture. It checks compiled Java programs ("bytecode") for well-formedness to prevent runtime errors (and thus potential attacks) like stack underflow or overflow. Despite its central role in the Java security architecture, for a long time the JBV was not well understood and its implementations by Sun and Microsoft contained security-critical bugs. Gerwin Klein was the first to formally verify a (functional) implementation of a byetcode verifier for Java. This won him the 2003 Dissertation Prize of the Gesellschaft für Informatik.
This course is about applications of logic to programming. The goal is to prove program properties by logical deductions and to build tools that support and automate these deductions. To this end we introduce the theorem prover Isabelle by T. Nipkow (Munich University) and Larry Paulson (Cambridge University).
Isabelle is a so called interactive theorem prover. It supports the proof of arbitrary mathematical theorems in a dialogue between user and machine. The user describes the overall structure of the proof in a programming language like notation, the system checks the correctness of each step and tries to fill in missing details.
Two typical examples from computer science and mathematics demonstrate the wide spectrum of possible applications of Isabelle:
Program of the course:
1. Motivating formal methods:the Hotel Key Cards system:
1.1 The Hotel Key Cards System
1.2 Goals of Formal Systems
1.3 Isabelle, a generic tool for formal verification.
2. An overview of Isabelle:
2.2 Types, Terms and ?-calculus.
2.3 Type inference and basic types
2.4 Theories and interface (Proof General)
3. Recursion, induction, types and function definition in Isabelle :
3.1. Recursion and Induction on Lists.
3.2. Proofs and Meta-Logic.
3.3 Type definition and datatypes in Isabelle.
3.4. Function definition in Isabelle.
4. Proofs by simplification in Isabelle:
4.1 Term rewriting and schematic variables.
4.2 Term rewriting in Isabelle:
4.3 Extension of rewriting.
5. Formalizing the Hotel Key Cards system in Isabelle.
5.1 Basic Types of the system
5.2 States and reachable states.
5.3 Possible events of the system
6. Proving the correctness of the Hotel Key Cards system:
6.1 Goal and Proof Style.
6.2 Issued Keys Lemmas.
6.3 No Key Reusing Lemmas, No Unauthorized Recoding Lemma.
6.4 Safe Rooms Lemmas.
6.5 Main Theorem.
We thank the local organizers of the school, Prof. Cristina Baroglio and Simona Ronchi, for making this short course possible, and for all their help.
We especially thank Prof. Tobias Nipkow, of University of Munich, Germany, for providing the original course material.
Isabelle Home Page:
Isabelle Book: “A Proof Assistant for Higher Order Logic’’ by T. Nipkow, L. Paulson, M. Wenzel, on LNCS 2283. Free Download from Isabelle Home Page.
The Hotel Key Card exercise is taken from: Daniel Jackson ‘‘Software Abstraction. Logic, Language and Analysis’’ MIT Press 2006.
Follow the instruction from Isabelle site. Isabelle requires Linux, or, under Windows, a Linux emulator, like Cygwin.
If you have Windows, the fastest way of getting started is dowloading the file ``IsaMorph’’ (IsaMorph_0.2.1.iso).
Uncompress IsaMorph and save it on a CD. Rebooting your computer with this CD, you get a emulator of Linux and Isabelle. In order to save changes you need a read&write CD, or some external memory like an USB key, or a partition of your Hard Disk having some area for Linux.