Lab 1: StatDB

This lab assignment will introduce you to state abstraction.

In this lab assignment, you will implement a database that supports adding numbers and getting the mean of the numbers added so far. The specification will keep track of all numbers added, but the implementation will just keep track of two variables (the sum and the count of numbers seen so far). Your proof will connect your implementation to the specification.

To get started, commit your work in the class repo locally and run git pull to merge in the new lab. Run make to compile the starter code for the lab.

We've provided a CLI to test your implementation, although we will only be checking your proof. You can try running it before starting the lab by running make bin/statdb-cli followed by ./bin/statdb-cli, which should successfully build if your Coq and Haskell setup is working.

We recommend that you begin by reading the documentation for StatDB. We recommend reading the coqdoc in the following order:

1. Start with the StatDB API.
2. Next, read the API for the Variables module. You'll be implementing the StatDB using this API for storing the StatDB state.
3. Finally, read through the StatDB Implementation documentation. Some of this implementation is provided, as well as some starter code for the proofs. The assignment is to complete the exercises in this file.

When you are done with the lab assignment, run make lab1-handin.tar.gz to generate a lab1-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.