Lab 0: Hoare logic

This lab will introduce you to the use of Hoare logic to reason about the correctness of code.

To get started, clone the class repo at https://github.com/mit-pdos/6.826-2019-labs. Run make to build the starter code for the lab.

We recommend you begin by understanding the basics of the POCS infrastructure. The coqdoc documentation for the POCS module gives an overview, which is a good place to start. For the purposes of this lab, you can ignore the disk model.

Next, read the documentation for the lab. We recommend reading the coqdoc in the following order:

1. Start with the variables API.
2. Next, look at the the Exercises.v file. You'll be writing various procedures, specifications, and proofs in this file.

Once you have familiarized yourself with the reading, open up src/Lab0/Exercises.v and start working on the exercises for this lab.

When you are done with the lab assignment, run make lab0-handin.tar.gz to generate a lab0-handin.tar.gz file, and submit it via the submission web site.

Questions or comments regarding 6.826? Contact us on Piazza or send e-mail to the 6.826 staff at 6826-staff@lists.csail.mit.edu.