Preface
Welcome
- 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.
- 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!
Practicalities
System Requirements
- opam update (as necessary)
- opam install coq-vst.2.10 (this will take 30 minutes or more)
Downloading the Coq Files
Installation
Exercises
- 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).
Recommended Citation Format
@book {Appel:SF5,
author = {Andrew W. Appel, Lennart Beringer, and Qinxiang Cao},
editor = {Benjamin C. Pierce},
title = "Verifiable C",
series = "Software Foundations",
volume = "5",
year = "2023",
publisher = "Electronic textbook",
note = {Version 1.2.2, \URL{http://softwarefoundations.cis.upenn.edu} },
}
For Instructors and Contributors
Thanks
Check for the right version of VST
Require Import Coq.Strings.String.
Open Scope string.
Require Import VST.veric.version. (* If this line fails, it means
you don't have a VST installed. *)
Definition release_needed := "2.11.1".
Goal release = release_needed.
reflexivity ||
let need := constr:(release_needed) in let need := eval hnf in need in
let rel := constr:(release) in let rel := eval hnf in rel in
fail "The wrong version of VST is installed. You have VST version"
rel "but this version of 'Software Foundations Volume 5: Verifiable C'"
"demands version" need ". If possible, install VST version" need
"using the Coq Platform or using opam. Or, if not from Coq Platform or opam,"
"for instructions about building VST from source and accessing that version, see the README file in this directory."
"Or, instead of installing VST" need ","
"if you want to proceed using VST version" rel ","
"then edit the Definition release_needed in Preface.v".
Abort.
Require Import ZArith.
Local Open Scope Z_scope.
Require VC.stack. (* If this line fails, do 'make stack.vo' *)
Goal VC.stack.Info.bitsize = VST.veric.version.bitsize.
reflexivity ||
let b1 := constr:(VST.veric.version.bitsize) in let b1 := eval compute in b1 in
let b2 := constr:(VC.stack.Info.bitsize) in let b2 := eval compute in b2 in
fail "Your installed VST is configured to verify C programs compiled with"
b1 "bit pointers,"
"but the .c files in the local directory have been clightgen'ed as if compiled with"
b2 "bit pointers."
"You can fix this by executing the shell command, "
"bash cfiles-bitsize" b1 " to install the properly configured clightgen outputs."
"It is not necessary to have clightgen installed".
Abort.
(* 2023-03-25 11:30 *)
Open Scope string.
Require Import VST.veric.version. (* If this line fails, it means
you don't have a VST installed. *)
Definition release_needed := "2.11.1".
Goal release = release_needed.
reflexivity ||
let need := constr:(release_needed) in let need := eval hnf in need in
let rel := constr:(release) in let rel := eval hnf in rel in
fail "The wrong version of VST is installed. You have VST version"
rel "but this version of 'Software Foundations Volume 5: Verifiable C'"
"demands version" need ". If possible, install VST version" need
"using the Coq Platform or using opam. Or, if not from Coq Platform or opam,"
"for instructions about building VST from source and accessing that version, see the README file in this directory."
"Or, instead of installing VST" need ","
"if you want to proceed using VST version" rel ","
"then edit the Definition release_needed in Preface.v".
Abort.
Require Import ZArith.
Local Open Scope Z_scope.
Require VC.stack. (* If this line fails, do 'make stack.vo' *)
Goal VC.stack.Info.bitsize = VST.veric.version.bitsize.
reflexivity ||
let b1 := constr:(VST.veric.version.bitsize) in let b1 := eval compute in b1 in
let b2 := constr:(VC.stack.Info.bitsize) in let b2 := eval compute in b2 in
fail "Your installed VST is configured to verify C programs compiled with"
b1 "bit pointers,"
"but the .c files in the local directory have been clightgen'ed as if compiled with"
b2 "bit pointers."
"You can fix this by executing the shell command, "
"bash cfiles-bitsize" b1 " to install the properly configured clightgen outputs."
"It is not necessary to have clightgen installed".
Abort.
(* 2023-03-25 11:30 *)