Welcome
Here's a good way to build formally verified correct software:
- Write your program in an expressive language with a good proof theory
(the Gallina language embedded in Coq's logic).
- Prove it correct in Coq.
- Extract it to ML and compile it with an optimizing ML compiler.
Unfortunately, for some applications you cannot afford to use a higher-order
garbage-collected functional programming language such as Gallina or ML.
Perhaps you are writing an operating-system kernel, or a bit-shuffling
cryptographic primitive, or the runtime system and garbage-collector of
your functional language! In those cases, you might want to use a low-level
imperative systems programming language such as C.
But you still want your OS, or crypto, or GC, to be correct! So you should
use machine-checked program verification in Coq. For that purpose, you can
use
Verifiable C, a program logic and proof system for C.
What is a program logic? One example of a program logic is the Hoare
logic that you studied in the
Programming Language Foundations
volume of this series. (If you have not done so already, study the
Hoare and Hoare2 chapters of that volume, and do the exercises.)
Verifiable C is based on a 21st-century version of Hoare logic called
higher-order impredicative concurrent separation logic. Back in
the 20th century, computer scientists discovered that Hoare Logic was
not very good at verifying programs with pointer data structures; so
separation logic was developed. Hoare Logic was clumsy at
verifying concurrent programs, so
concurrent separation logic was
developed. Hoare Logic could not handle higher-order object-oriented
programming patterns or function-closures, so
higher-order
impredicative program logics were developed.
This electronic book is Volume 5 of the
Software Foundations series,
which presents the mathematical underpinnings of reliable software. The
principal novelty of
Software Foundations is that it is one hundred
percent formalized and machine-checked: the entire text is literally a
script for Coq. It is intended to be read alongside an interactive
session with Coq. All the details in the text are fully formalized in Coq,
and the exercises are designed to be worked using Coq.
Before studying this volume, you should be a competent user of Coq:
- Study Software Foundations Volume 1 (Logical Foundations), and
do the exercises!
- Study the Hoare and Hoare2 chapters of
Software Foundations Volume 2 (Programming Language Foundations), and
do the exercises!
- Study the Sort, SearchTree, and ADT chapters of
Software Foundations Volume 3 (Verified Functional Algorithms), and
do the exercises!
You will also need a working knowledge of the C programming language.
Practicalities
System Requirements
Coq runs on Windows, Linux, and OS X. The Preface of Volume 1
describes the Coq installation you will need. This edition was
built with Coq 8.12.0.
You will need VST installed. You can do that either by installing
it as part of the standard "Coq Platform" that is released with each
new version of Coq, or using opam (the package is named coq-vst).
At the end of this chapter is a test to make sure you have the right
version of VST installed.
IF YOU USE OPAM, the following opam commands may be useful:
- opam repo add coq-released https://coq.inria.fr/opam/released
- opam pin coq 8.13.0
- opam install coq-vst.2.7 (this will take 30 minutes or more)
- (to use coqide:) opam pin lablgtk3 3.0.beta5
- (to use coqide:) opam install coqide
You do not need to install CompCert clightgen to do the exercises
in this volume. But if you wish to modify and reparse the .c files,
or verify C programs of your own, install the CompCert verified
optimizing C compiler. You can get CompCert from compcert.inria.fr,
or (starting with Coq 8.12) in the standard "Coq Package" or by
opam (the package is named coq-compcert).
Downloading the Coq Files
A tar file containing the full sources for the "release version"
of this book (as a collection of Coq scripts and HTML files) is
available at
https://softwarefoundations.cis.upenn.edu.
(If you are using the book as part of a class, your professor may
give you access to a locally modified version of the files, which
you should use instead of the release version.)
Installation
Unpack the
vc.tgz tar file into a vc directory.
In this
vc directory, the
make command builds it.
Exercises
Each chapter includes exercises. Each is marked with a
"star rating," which can be interpreted as follows:
- One star: easy exercises that underscore points in the text
and that, for most readers, should take only a minute or two.
Get in the habit of working these as you reach them.
- Two stars: straightforward exercises (five or ten minutes).
- Three stars: exercises requiring a bit of thought (ten
minutes to half an hour).
- Four and five stars: more difficult exercises (half an hour
and up).
Please do not post solutions to the exercises in any public place:
Software Foundations is widely used both for self-study and for
university courses. Having solutions easily available makes it
much less useful for courses, which typically have graded homework
assignments. The authors especially request that readers not post
solutions to the exercises anyplace where they can be found by
search engines.
Recommended Citation Format
If you want to refer to this volume in your own writing, please
do so as follows:
@book {Appel:SF5,
author = {Andrew W. Appel and Qinxiang Cao},
title = "Verifiable C",
series = "Software Foundations",
volume = "5",
year = "2021",
publisher = "Electronic textbook",
note = {Version 1.0.0, \URL{http://softwarefoundations.cis.upenn.edu} },
}
For Instructors and Contributors
If you plan to use these materials in your own course, you will
undoubtedly find things you'd like to change, improve, or add.
Your contributions are welcome! Please see the
Preface
to
Logical Foundations for instructions.
