Specification of variables.

This layer describes mutable variables. In this lab assignment, we will be assuming that this layer is already provided for us, and that its implementation meets its specification. Your job will be to familiarize yourself with the lab infrastructure by writing procedures, specifications, and proofs for code on top of these mutable variables. There are three variables, which we will call x, y, and z. To refer to a particular variable name, we use this type.

The values of these variables comprise the state:

StateVar extracts a particular variable by its var name from a State.

Operations on variables.

We provide two operations for dealing with variables: reading a variable and writing a value to a variable. To meaningfully write code on top of these variables, it's important to know what reading and writing a variable does. We will capture this with the following specifications. The specification for reading a variable, read_spec, is parametrized by the variable that we are reading, v.

The precondition is True, reflecting the fact that it's always OK to read any variable v.

The postcondition has two parts to it. First, it says that the resulting state after reading a variable, state', is the same as the state before reading the variable, state. In other words, reading a variable doesn't change the state.

The second part of the postcondition says that the return value r is the value of the variable v in the state.

Since our framework supports reasoning about crashes, we must supply a recovered condition, but here we will ignore crashes by saying that recovery can never occur, by stating False.

The specification for writing a variable, write_spec is parametrized by two things: the variable being modified, v, and the value being written to that variable, val. The precondition and recovery condition are the same as for reading (True and False respectively).

The postcondition says that the return value is always equal to tt (a way of representing a procedure that has no return value), and

the new state, state', is updated based on which variable we were trying to modify.

Variables module

An implementation of variables must implement the following module type and must prove that that its code implements the spec correctly using refinement. If we were to implement this module in Haskell, we would provide Haskell code for read and write, and ensure that this code meets the required specification. For this lab assignment, we will simply assume that such an implementation exists, and focus on writing code, specs, and proofs in the lab infrastructure. In the next lab assignment, you will use a similar variables layer that supports extraction to Haskell, and allows you to really run your programs.