Examples and exercises from the book Program Proofs by K. Rustan M. Leino translated to Rust and verified with Prusti, a deductive verifier for Rust programs developed at ETH Zurich.
Each chapter of the book that we have translated can be found in its own crate at the root of this repository.
Each crate can be verified, as a whole, using cargo prusti from the command line or using the Prusti Assistant extension for VS Code.
Within each crate, there are two main subdirectories of interest:
(chapter)/src/examples- contains translated examples, i.e. various snippets of code from the given chapter;(chapter)/src/exercises- contains translated exercises, i.e. (possible) solutions to the exercises from the given chapter.
Files in these subdirectories follow the naming scheme example_(section)_(subsection).rs or exercise_(section)_(subsection).rs. The remaining files in each crate serve to configure Prusti, configure Cargo, and to tie together the example and exercise files.
| Chapter | Notes | |
|---|---|---|
| PART 0 | Learning the Ropes | |
| Chapter 1 | Basics | |
| Chapter 2 | Making it Formal | |
| Chapter 3 | Recursion and Termination | Termination checking is not yet supported in Prusti |
| Chapter 4 | Inductive Datatypes | |
| Chapter 5 | Lemmas and Proofs | Ghost code is not yet supported in Prusti |
| PART 1 | Functional Programs | |
| Chapter 6 | (Skipped) | |
| Chapter 7 | (Skipped) | |
| Chapter 8 | Sorting | |
| Chapter 9 | Modules | |
| Chapter 10 | (Skipped) | |
| PART 2 | Imperative Programs | |
| Chapter 11 | (Skipped) | |
| Chapter 12 | (Skipped) | |
| Chapter 13 | (Skipped) | |
| Chapter 14 | Modifying Arrays | |
| Chapter 15 | (Skipped) | |
| Chapter 16 | Objects | |
| Chapter 17 | Mutable Data Structures |
The translations found in this repository were developed as part of Patrick Muntwiler's BSc thesis.
- Muntwiler, Patrick. "Evaluating and Documenting a Rust Verifier." (2023).