program-proofs-gobra

Examples and exercises from the book Program Proofs by Rustan Leino translated to Go and verified with Gobra.

Repository Structure

For each chapter of the book that we cover, we have a separate package. In each package, there are two kinds of files depending on their names:

• files named examples_X.Y.gobra contain the examples from section X.Y of the book.
• files named exercises_X.Y.gobra contain the solutions to the exercises from section X.Y of the book, not the solution to exercise X.Y.

Current Status

So far, we have translated the examples and exercises from Part 0 and are in the process of translating those from Part 1 and 2. These will be added gradually to this repository.

References

• Egli, Timon. "Translating Pedagogical Exercises to Viper’s Go Front-end." (2023).