An abstract data type (ADT) can be defined as a set of values together with some operations. From the perspective of formal verification, the specifications of those operations should also be a part of an ADT. When we implemented BSTs in SearchTree, we saw that maintaining a representation invariant was important to rule out trees that could never be constructed through operations of the data structure. That invariant became a precondition for many operations, though there was no need for clients of the data structure to know any details of the invariant. In this chapter we'll study a little of Coq's module system, which enables hiding some details of the implementation of an ADT, while also exposing the formal specification of the ADT. Some prior knowledge of an ML-style module system, especially OCaml's, will be helpful. Here are some sources that cover it:

• Introduction to Objective Caml, chapters 12 and 13. Jason Hickey, 2008. Available from https://ocaml.org/learn/books.html.
• The OCaml System Manual, chapter 2. Xavier Leroy et al., 2020. Available from http://caml.inria.fr/pub/docs/manual-ocaml/.

The Table ADT

An association table is an ADT that binds keys to values. There are many other names for this concept, including map. We've already used that name before, though, for a specific data structure using higher-order functions. So for clarity in this chapter we use table. Below is a Coq Module Type that declares an interface for the table ADT. A parameter is like a definition, except it declares only the type of an identifier, not the value to which it is bound. An axiom is similarly like a theorem, except no proof is provided.

A table is a binding from keys to values. It is total, meaning it binds all keys.

Keys are natural numbers.

Values are an arbitrary type V.

The default value to which keys are bound.

empty is the table that binds all keys to the default value.

get k t is the value v to which k is bound in t.

set k v t is the table that binds k to v and otherwise has the same bindings as t.

The following three axioms are an equational specification for the table ADT.

Implementing Table with Functions

We can implement Table with a Module that is parameterized on the type of values -- or, rather, parameterized on a module that contains such a type. A parameterized module is also called a functor. Module type ValType says that there must be a type named V, with a default value provided:

Functor FunTable takes as input a module of type ValType, which must therefore contain a type V. As output, FunTable produces a module of type Table. By writing <: Table, below, we ask Coq to check that the output module contains all the components required by Table.

A table is a function from keys to values.

The implementation must prove the theorems that the interface specified as axioms.

As an example, let's instantiate FunTable with strings as values.

Exercise: 2 stars, standard, optional (NatFunTableExamples)

Define a module that uses FunTable to implement a table mapping keys to values, where the values have type nat, with a default of 0. Write unit tests to check the operation of get and set.

Implementing Table with Lists

Exercise: 3 stars, standard (lists_table)

Use association lists to implement Table.

Instantiate your table and prove the following facts.

Implementing Table with BSTs

Tables implemented with functions and association lists are, of course, inefficient. For a more efficient implementation, we can use BSTs.

The three basic equations we proved about tree in SearchTree make short work of the theorems we need to prove for Table.

Tables with an elements Operation

Now let's consider a richer interface ETable for Tables that support bound and elements operation.

A First Attempt at ETable

Include, as the name suggests, includes all the declarations from Table. Not only does that save keystrokes, it also means if we ever update Table to have new operations or new types, they automatically get included here, too.

We proved in SearchTree that the BST elements operation is correct and complete. So we ought to be able to implement ETable with BSTs. Let's try.

Include all the definitions from TreeTable, instantiated on VT.

Thanks to the Include, we now have all the tree operations defined "for free" in this module. For example:

pose proof t as H is equivalent to assert (H : ...the type of t...). { apply t. } but saves some keystrokes.

Stuck! We don't know that t satisfies the BST invariant.

Again stuck because of the BST invariant.

A Revised ETable

To prove that elements is correct, we need to know that trees satisfy the BST invariant. So, we declare a function rep_ok in the interface, and use it as a precondition for values of type table. We also add axioms to state that the ADT operations produce values that satisfy the representation invariant, i.e., it is a postcondition. And, we add a specification of bound.

empty and set produce valid representations.

The specification of bound:

The specification of elements:

Now we can use the table.

Encapsulation with the Coq Module System (Advanced)

Functor TreeETable, above, reveals internal implementation details that your data structures class probably taught you are better kept private. For example, the constructors E and T of trees and the implementation of get are publicly exposed:

Like many languages, Coq makes it possible to encapsulate these details, meaning that they become hidden outside the module. It's a simple matter of changing the <: syntax to : in the functor's type. The only change in the implementation below is that one character. The : syntax makes the module type opaque: only what is revealed in the type is available for code outside the module to use. The <: syntax, however, makes the module type transparent: the module must conform to the type, but everything about the module is still revealed.

Unfortunately, the module is now too encapsulated to be useful:

The problem is that the module now hides not only the internal implementation, but also the value type V. The functor was instantiated on StringVal, which defines that type as string. But the output of the functor has type ETable, which doesn't reveal anything about V except that it is a Type. Note in the output of the following command how V is printed like an axiom would be, indicating that nothing is known (externally) about its implementation:

We need to selectively expose certain implementation details. We've just seen that V should be exposed. Along with it, we'll also want default to be exposed. We can accomplish that with an advanced feature of Coq's module system. The Coq manual doesn't give this feature a name, but OCaml (in which Coq is implemented) calls it a sharing constraint, so we'll use that term here. A sharing constraint enables us to constrain definitions shared by modules to be the same.

Putting sharing constraints to use, let's expose V and default in our implementation of tree-based tables.

Note what we've happily achieved: we can reason about the behavior of an ADT entirely from its specification, rather than depending on the implementation code. This is what specification comments in interfaces attempt to achieve in real-world code.

Exercise: 4 stars, advanced, optional (elements_spec)

Develop a nicely-encapsulated interface and implementation of tree-based tables that exposes the rest of the specification of elements from SearchTree, including the inverses of correctness and completenesss, sortedness, and non-duplication. Send us your solution, so we can include it! ☐

Model-based Specification

The interfaces above have been based on equational specification of tables. Let's consider model-based specifications. Recall from SearchTree that in this style of specification, we

• introduce an abstraction function (or relation) that associates a concrete value of the ADT implementation with an abstract value in an already well-understood type; and
• show that the concrete and abstract operations are related in a sensible way.

We begin by defining a new map operation, bound, and redefining existing operations to make them more clear in the table specification we are about to write.

Now we can define an interface for tables that includes an abstraction function Abs, and specifications written in terms of it.

Exercise: 4 stars, standard (list_etable_abs)

Implement ETableAbs using association lists as the representation type.

Exercise: 3 stars, standard, optional (TreeTableModel)

Give an implementation of ETableAbs using the abstraction function Abs from SearchTree. All the proofs of the relate axioms should be simple applications of the lemmas already proved as exercises in that chapter.

Exercise: 2 stars, advanced, optional (TreeTableModel')

Repeat the previous exercise, this time using the alternative Abs' function from SearchTree. Hint: Just tweak your solution to the previous exercise. ☐

Summary of ADT Verification

With equational specifications:

• Define a representation invariant to characterize which values of the representation type are legal. Prove that each operation on the representation type preserves the representation invariant.
• Using the representation invariant, verify the equational specification.

With model-based specifications:

• Define and verify preservation of the the representation invariant.
• Define an abstraction function that relates the representation type to another type that is easier to reason about.
• Prove that operations of the abstract and concrete types commute with the abstraction function.

Another ADT: Queue

Here is an interface and algebraic specification for FIFO queues. To ensure totality, peek takes a default value and deq returns the empty queue when applied to the empty queue.

Exercise: 3 stars, standard (list_queue)

Implement that interface and verify your implementation. As the representation type, use list V. At least one operation will have to be linear time; we recommend that it be enq. All the proofs should be quite easy.

Here is an interface and model-based specification for queues. We omit rep_ok from it, because our intended implementation isn't going to require a representation invariant.

Exercise: 3 stars, standard (two_list_queue)

Below is an implementation of QueueAbs using two lists. It achieves amortized constant-time performance, improving on the single-list implementation. Verify this implementation.

Representation Invariants and Subset Types

In specifications thus far, whenever there was a representation invariant that needed to be enforced we had to add it as a precondition and postcondition for operations. For example, the correctness of the table get operation depended on its table input satisfying rep_ok. We had to write propositions like ∀ (t : table), rep_ok t → ..., in which we had a type table with lots of values, and we got rid of some of those values by requiring rep_ok to hold of them. Coq makes it possible to directly express the requirement that values of a type must satisfy a proposition. The type
      {x : A | P} is the type of all values x of type A that satisfy property P, which itself has type A → Prop. The notation is deliberately suggestive of set-builder notation used in mathematics. Such types are known as subset types.

Example: The Even Naturals

We can define the subset type of even natural numbers using the property Nat.Even from the standard library:

But when we try to say that 2 is an even_nat, Coq rejects the definition:

The problem is that 2 is a nat, but we haven't proved Nat.Even 2. The proof is easy:

Now we can provide that proof to convince Coq two is an even_nat. We can do that with function exist, which is suggestive of "there exists an x : A such that P x."

Another way of constructing two is to enter Coq's proof scripting mode and use tactics. We saw this briefly in ProofObjects.

That technique is often useful with subset types, because it helps us more easily build the proof objects, rather than have to write them ourselves. A value of type even_nat is like a "package" containing the nat and the proof that the nat is even. We have to use functions to extract those components from the package.

Defining Subset Types

Like nearly everything else we've seen in Coq's logic, subset types are actually defined in the standard library rather than being built-in to the language.

Subset types are just a syntactic notation for sig:

The name sig is short for the Greek capital letter sigma, because subset types are similar to something known in type theory as sigma types, aka dependent sums. Subset types and existential quantification are quite similar. Recall how the latter is defined:

The only difference is that sig creates a Type whereas ex creates a Prop. That is, the former is computational in content, whereas the latter is logical. Therefore we can pattern match to recover the witness from a sig, but we cannot do the same with an ex.

Example: Vectors

A vector is a list of a known length. Type vector X contains values (xs, n) with a particular representation invariant: n must be the length of xs.

The type itself enforces the representation invariant, because a value of type vector X cannot be constructed without first proving that the invariant holds.

Exercise: 1 star, standard (a_vector)

Construct any vector of your choice.

Exercise: 2 stars, standard (vector_cons_correct)

Define a cons operation on vectors. Remember to end with Defined rather than Qed.

Prove the correctness of your cons operation.

Exercise: 2 stars, standard (vector_app_correct)

Define an append operation on vectors.

Prove the correctness of your append operation.

Using Subset Types to Enforce the BST Invariant

Let's use subset types to reimplement tree-based tables with an elements operation. Previously we had to add rep_ok to the interface and specifications. With subset types we can eliminate that.

Note: no rep_ok anywhere.

table now is required to enforce BST.

Now instead of proving separate theorems that operations return valid representations, the proofs are "baked in" to the operations.

Now we insert a projection to get to the tree.

Now the rest of the proofs require minor modifications to destruct the table to get the tree and the representation invariant, and use the latter where needed.