Let's consider the concept of lookup tables, indexed by keys that are natural numbers, mapping those keys to values of arbitrary (parametric) type. We can express this in Coq as follows:

This means: in any Module that satisfies this Module Type, there's a type table of lookup-tables, a type V of values, and operators empty, get, set that satisfy the axioms gempty, gss, and gso. For example, we can easily give an implementation of TABLE in terms of our function-based maps. For specificity, we'll take V to be the type bool and use a default value of false.

The specialization of TABLE to TABLE_STRING exposes the definition of V as string to the world outside the module. Without it, all that would be known is what TABLE exposes, which is that V is some Type. Now, let's calculate: put (1,true) and then (3,false) into a map, then lookup 1.

An Abstract Data Type comprises:

• A type with a hidden representation (in this case, t).
• Interface functions that operate on that type (empty, get, set).
• Axioms about the interaction of those functions (gempty, gss, gso).

So, MapsTable is an implementation of the TABLE abstract type.

Exercise: 4 stars, standard (ListsTable)

Give an alternative implementation of TABLE using lists of (key,value) pairs as the hidden representation. Again, take V to be bool and default to be false.

The problem with MapsTable and ListsTable is that they are each very inefficient: linear time per get operation. If you do a sequence of N get and set operations, it can take time quadratic in N. For a more efficient implementation, we can use our search trees from SearchTreeAlt.

Now let's consider a richer interface ETABLE for Tables that support an elements operation.

Since we know our search tree implementation supports elements, let's try to use it:

Giving proofs of the specifications involving elements requires that t have the BST property. This is a common problem with ADTs: we need values of the (hidden) representation type to be well-formed, i.e. to satisfy some invariant. ALthough we know that the official operations on ADTs do maintain the invariant, we must ensure that the client of an ADT cannot "forge" values, that is, cannot coerce the representation type into the abstract type; especially ill-formed values of the representation type. This "unforgeability" is enforced in some real programming languages: ML (Standard ML or Ocaml) with its module system; Java, whose Classes can have "private variables" that the client cannot see.

A Brief Excursion into Dependent Types

Let's briefly look at a different way of enforcing the representation invariant: every value of the representation type will carry along with it a proof that the value satisfies the representation invariant. To do this, we'll use sigma types, aka dependent sums, which are defined in the Coq standard library. Suppose P is a predicate on type A, that is, P : A → Prop. Then sig A P is the type of elements of A that satisfy P. You could think of this as a subset: sig A P is the subset of values of A that satisfy P. Based on that intuition, there is a notation {x : A | P} that means sig A P.

We'll apply that idea to search trees. The type A will be tree V. The predicate P(x) will be BST(x).

Now: t is a package with two components: The first component is a tree, and the second component is a proof that the first component has the SearchTree property. We can destruct t to see that more clearly.

Exercise: 4 stars, advanced, optional (ListsETable)

Another simple (though inefficient) representation of an ETABLE is as a list of (key,value) pairs, without duplicate key values (but not necessarily sorted). Using TreeETable2 as a model, write a module definition Module ListsETable <: ETABLE that uses dependent types to enforce the no-duplicates invariant.

(End of the brief excursion into dependent types.)

Abstracting over invariants.

Even without using dependent types, we can build the requirement for representation invariants into module signatures. Of course, we do not want the details of the invariant to be visible as part of the signature. The trick is to specify the existence of an invariant and the fact that it is maintained by suitable operations and required by others, while leaving the actual definition of the invariant abstract. For example, we can modify the ETABLE signature to use this approach as follows. 1. We introduce an abstract invariant is_table: table → Prop as a new parameter of the signature. 2. We add axioms specifying that empty tables obey the invariant and that set operations maintain the invariant. 3. We add assumptions to the specifications for gie, ieg, and edistinct to require that the invariant holds.

Now we can prove that our search trees match this extended signature, by instantiating the abstract invariant with the BST property, and invoking the lemmas we proved in SearchTree to show that this property is correctly maintained. The proofs of the elements-related specifications now take a BST assumption, and go through easily.

Module signatures for model-based Specification

Finally, let's reconsider the model-based specification for search trees that we developed towards the end of SearchTree. Recall that in this style of specification, we introduce an abstraction function (or more generally relation) that associates each concrete value of the ADT implementation with a value in a more abstract, already well-understood, type, and shows that the concrete and abstract operations are related in a sensible way. In the case of seach trees, you showed (in some exercises) that we can relate each tree to a functional partial map, such that lookup and insert operations on the tree correspond to find and update operations on the map. We can capture this approach in a module signature by adding the abstraction function as a parameter and the lemmas involving it as axioms. Note that the abstraction function can remain abstract in the signature! That is, we don't really care how the abstraction function works, as long as it lets us prove the lemmas.

Exercise: 3 stars, standard (TreeTableModel)

Give an implementation of ETABLE_INV_MODEL 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. Again, take V to be bool and default to be false.

Exercise: 2 stars, advanced, optional (TreeTableModel2)

Repeat the previous exercise, this time using the alternative Abs' function from SearchTree. Hint: This requires only very small changes from the previous exercise's solution!

Summary of Abstract Data Type Proofs

Step 1. Define a representation invariant. (In the case of search trees, the representation invariant is the BST predicate.) Prove that each operation on the data type preserves the representation invariant. For example:

Notice two things: Any operator (such as insert) that takes a tree parameter can assume that the parameter satisfies the representation invariant. That is, the insert_BST theorem takes a premise, BST t. Any operator that produces a tree result must prove that the result satisfies the representation invariant. Thus, the conclusions, BST (empty_tree V) and BST (insert k v t) of the two theorems above. Finally, any operator that produces a result of "base type", has no obligation to prove that the result satisfies the representation invariant; that wouldn't make any sense anyway, because the types wouldn't match. That is, there's no "lookup_BST" theorem, because lookup doesn't return a result that's a tree. Step 2 (only if using model-based specification). Define an abstraction relation. (In the case of search trees, it's the Abs function.) This relates the data structure to some mathematical value that is (presumably) simpler to reason about.

For each operator, prove that: assuming each tree argument satisfies the representation invariant and the abstraction relation, prove that the results also satisfy the appropriate abstraction relation.

Step 3. Using the representation invariant, pove that all the axioms of your ADT are valid. For example...

Exercise in Data Abstraction

The rest of this chapter is optional.

Here's the Fibonacci function.

Here's a silly little program that computes the Fibonacci function.

Here's a strange "List" module.

Module L implements approximations of lists: it can remember the first three elements, and forget the rest. Now watch:

This little theorem may be useful in the next exercise.

Exercise: 4 stars, standard, optional (listish_abstraction)

In this exercise we will not need a representation invariant. Define an abstraction relation:

Now, we will make these operators opaque. Therefore, in the rest of the proofs in this exercise, you will not unfold their definitions. Instead, you will just use the theorems create_relate, cons_relate, nth_relate.

Exercise: 2 stars, standard, optional (fib_time_complexity)

Suppose you run these three programs call-by-value, that is, as if they were ML programs. fibonacci N fib N fibish N What is the asymptotic time complexity (big-Oh run time) of each, as a function of N? Assume that the plus function runs in constant time. You can use terms like "linear," "N log N," "quadratic," "cubic," "exponential." Explain your answers briefly. fibonacci: (* fill in here *)
fib: (* fill  in here *)
fibish: (* fill in here *)
☐