Skip to main content
main-content

Über dieses Buch

Part I of this book is a practical introduction to working with the Isabelle proof assistant. It teaches you how to write functional programs and inductive definitions and how to prove properties about them in Isabelle’s structured proof language. Part II is an introduction to the semantics of imperative languages with an emphasis on applications like compilers and program analysers. The distinguishing feature is that all the mathematics has been formalised in Isabelle and much of it is executable. Part I focusses on the details of proofs in Isabelle; Part II can be read even without familiarity with Isabelle’s proof language, all proofs are described in detail but informally.

The book teaches the reader the art of precise logical reasoning and the practical use of a proof assistant as a surgical tool for formal proofs about computer science artefacts. In this sense it represents a formal approach to computer science, not just semantics. The Isabelle formalisation, including the proofs and accompanying slides, are freely available online, and the book is suitable for graduate students, advanced undergraduate students, and researchers in theoretical computer science and logic.

Inhaltsverzeichnis

Frontmatter

Isabelle

Frontmatter

Chapter 1. Introduction

Abstract
Isabelle is a generic system for implementing logical formalisms, and Isabelle/HOL is the specialization of Isabelle for HOL, which abbreviates Higher-Order Logic. We introduce HOL step by step following the equation.
Tobias Nipkow, Gerwin Klein

Chapter 2. Programming and Proving

Abstract
This chapter introduces HOL as a functional programming language and shows how to prove properties of functional programs by induction.
Tobias Nipkow, Gerwin Klein

Chapter 3. Case Study: IMP Expressions

Abstract
The methods of the previous chapter suffice to define the arithmetic and Boolean expressions of the programming language IMP that is the subject of this book. In this chapter we define their syntax and semantics, write little optimizers for them and show how to compile arithmetic expressions to a simple stack machine. Of course we also prove the correctness of the optimizers and compiler!
Tobias Nipkow, Gerwin Klein

Chapter 4. Logic and Proof Beyond Equality

Abstract
The core syntax of formulas (form below) provides the standard logical constructs, in decreasing order of precedence.
Tobias Nipkow, Gerwin Klein

Chapter 5. Isar: a Language for Structured Proofs

Abstract
Apply-scripts are unreadable and hard to maintain. The language of choice for larger proofs is Isar. The two key features of Isar are (1) It is structured, not linear. (2) It is readable without its being run because you need to state what you are proving at any given point. Whereas apply-scripts are like assembly language programs, Isar proofs are like structured programs with comments. A typical Isar proof looks like this.
Tobias Nipkow, Gerwin Klein

Semantics

Frontmatter

Chapter 6. Programming and Proving

Abstract
This chapter introduces HOL as a functional programming language and shows how to prove properties of functional programs by induction.
Tobias Nipkow, Gerwin Klein

Chapter 7. IMP: A Simple Imperative Language

Abstract
To talk about semantics, we first need a programming language. This chapter defines one: a minimalistic imperative programming language called IMP. The main aim of this chapter is to introduce the concepts of commands and their abstract syntax, and to use them to illustrate two styles of defining the semantics of a programming language: big-step and small-step operational semantics. Our first larger theorem about IMP will be the equivalence of these two definitions of its semantics. As a smaller concrete example, we will apply our semantics to the concept of program equivalence.
Tobias Nipkow, Gerwin Klein

Chapter 8. Compiler

Abstract
This chapter presents a first application of programming language semantics: proving compiler correctness. To this end, we will define a small machine language based on a simple stack machine. Stack machines are common lowlevel intermediate languages; the Java Virtual Machine is one example. We then write a compiler from IMP to this language and prove that the compiled program has the same semantics as the source program. The compiler will perform a very simple standard optimization for boolean expressions, but is otherwise non-optimizing.
Tobias Nipkow, Gerwin Klein

Chapter 9. Types

Abstract
This chapter introduces types into IMP, first a traditional programming language type system, then more sophisticated type systems for information flow analysis. Why bother with types? Because they prevent mistakes. They are a simple, automatic way to find obvious problems in programs before these programs are ever run.
Tobias Nipkow, Gerwin Klein

Chapter 10. Program Analysis

Abstract
Program analysis, also known as static analysis, describes a whole field of techniques for the static (i.e. compile-time) analysis of programs.
Tobias Nipkow, Gerwin Klein

Chapter 11. Denotational Semantics

Abstract
So far we have worked exclusively with various operational semantics which are defined by inference rules that tell us how to execute some command. But those rules do not tell us directly what the meaning of a command is. This is what denotational semantics is about: mapping syntactic objects to their denotation or meaning. In fact, we are already familiar with two examples, namely the evaluation of arithmetic and boolean expressions.
Tobias Nipkow, Gerwin Klein

Chapter 12. Hoare Logic

Abstract
So far we have proved properties of IMP, like type soundness, or properties of tools for IMP, like compiler correctness, but almost never properties of individual IMP programs. The Isabelle part of the book has taught us how to prove properties of functional programs, but not of imperative ones.
Tobias Nipkow, Gerwin Klein

Chapter 13. Abstract Interpretation

Abstract
In Chapter 10 we saw a number of automatic program analyses, and each one was hand crafted. Abstract Interpretation is a generic approach to automatic program analysis. In principle, it covers all of our earlier analyses. In this chapter we ignore the optimizing program transformations that accompany certain analyses.
Tobias Nipkow, Gerwin Klein

Backmatter

Weitere Informationen

Premium Partner

    Bildnachweise