To start with, we define a module called Exercises that takes as an argument an implementation of our variables layer, called vars.

Now that we are inside the module, we have access to the variables API that we defined in ThreeVariablesAPI. You can examine the functions provided by the vars module using the Check command, as follows:

The above Check command should have printed: vars.read : var -> proc nat meaning that vars.read is something that takes a variable name (of type var) and gives us a procedure that returns a nat value.

vars.write similarly takes a variable name and a new value and gives us a procedure with no return value.

Part A: incrementing and swapping.

To start with, we will define a simple procedure incX that increments the value of the x variable:

To check if we got the implementation right, let's try first testing it on a specific input. We can do this by writing a very particular specification: if the starting state was (1, 2, 3), corresponding to the values of variables x, y, and z respectively, then the final state should be (2, 2, 3). The vars.recover at the end of the specification says that we should run the vars.recover procedure after a crash; this does not matter so far, because we are ignoring crashes. The vars.abstr indicates how we are describing states in this specification. Here, states are described in terms of the variables layer (i.e., consisting of the three values for x, y, and z). We will see in the next lab how and why your specification may want to describe the state at a different abstraction layer.

Now your job is to state a more general specification for incX. It should take a precondition of True, as stated in the theorem below. Your task is to fill in the postcondition below so that it applies to any starting state, unlike the previous theorem that only worked for mkState 1 2 3. Then, prove your general specification correct. Replace Admitted. with Qed. when the proof is complete. When we grade, we basically check that your code compiles and that you didn't use Admitted. Take a look at the specifications in ThreeVariablesAPI.v if you're not sure where to start.

You have proven that the code of incX satisfies your specification in incX_ok, but how do you know if your specification is good enough? Did your specification omit any important details? One general approach is to try to use your specification to prove something. Let's do that now: prove that your specification above is sufficient to prove that running incX from state (5, 5, 5) gives us state (6, 5, 5). To use your incX_ok theorem from above, we tell the step_proc tactic about it by including it in the core hints database. To make sure that we don't accidentally look inside the code of incX, and thus force ourselves to prove statements about incX by relying on incX_ok, we mark it opaque using Opaque incX.

Swapping.

Here is another exercise, this time with you writing the code, the spec, and the proof. Implement a procedure swapXY that swaps the values of x and y; write a specification for it; and prove that your code meets the spec.

As a sanity check, prove that swapXY from state (2, 3, 4) gives you state (3, 2, 4).

Part B: recursive procedures.

In this last part of the lab assignment, you will reason about recursive procedures. To start with, we will give an example. We define a helper called addX that adds delta to the x variable.

Now, we define a procedure addX_list that takes a list of nats, and calls addX on each of them in turn.

To specify what we expect addX_list to do, we need to talk about the sum of values in a list. To do that, we define a Gallina function (purely in Coq) that computes the sum of values in a list.

Now we can state a specification about addX_list and prove it using induction. Note: You get an error "Expected a single focused goal but 2 goals are focused". For the labs, we turned on an option in Coq that enforces proofs use bullets (+, -, *) or curly braces { } to "focus" each line of the proof on a single goal. This makes proof scripts more manageable, which will help in later labs. If you get this error, make sure to use bullets or braces, the way you saw throughout Software Foundations.

Recursive procedures on your own.

For the final part, you will work out an example of recursive procedures on your own. Your job is to implement a procedure add_odds_evens that takes a list of nats, adds all of the even nats to variable x, and all of the odd nats to variable y. Implement add_odds_events in the recursive Fixpoint style that we used above in part C, write a spec for it, and prove it. Use Nat.even and Nat.odd to determine if a nat value is even or odd. You can use Search to locate helpful theorems about these, as follows:

To check your solution, prove this simple theorem about a particular execution of add_odds_evens using your spec. Add a Hint Resolve statement to let step_proc see your proven specification about add_odds_evens.