# Abstraction and Specification
This lab is all about writing, critiquing, and implementing specifications.
## The specification game
Suppose that an interface designer writes the following specification
for a function called `reverse`:
```
(* returns a list *)
val reverse : 'a list -> 'a list
```
This spec is clearly incomplete. For example, a devious programmer could meet
the spec with an implementation that gives the following output:
```
# reverse [1;2;3];;
- : int list = []
```
The designer, upon realizing this, refines the spec as follows:
```
(* reverse l returns a list that is the same length as l *)
val reverse : 'a list -> 'a list
```
But the devious programmer discovers that the spec still allows broken
implementations:
```
# reverse [1;2;3];;
- : int list = [0;0;0]
```
Finally, the designer settles on a third spec:
```
(* reverse l returns a list m satisfying
* - length l = length m
* - for all i, nth m i = nth l (n - i - 1) where n is the length of l
*)
val reverse : 'a list -> 'a list
```
With this spec, the devious programmer is forced to provide a working
implementation to meet the spec, so the designer has successfully
written her spec.
##### Exercise: spec game [✭✭✭]
Play the following game. You could play against yourself, but even
better would be to play against another student in this
or another programming course. One player
(the "clever specifier") writes a specification for a function. The
other player (the "devious programmer") tries to find holes in the
specification by coming up with an input/output pair for the function
that meets the specification but violates the intent of the function.
If the programmer can't come up with a bad example, then the specifier
wins. If not, the roles reverse and the other player makes an attempt
to write a specification.
Play this game with the following functions, whose spec is suggested
by their names. Alternate which player goes first.
- `num_vowels : string -> int`
- `is_sorted : 'a list -> bool`
- `sort : 'a list -> 'a list`
- `max : 'a list -> 'a`
- `is_prime : int -> bool`
□
## Specifying a data abstraction
Let's create a *data abstraction* (a module that represents some kind
of data) for single-variable integer polynomials of the form
\\[c_n x^n + \ldots + c_1 x + c_0.\\] Let's assume that the polynomials
are *dense*, meaning that they contain very few coefficients that are zero.
Here is an incomplete interface for polynomials:
```
(* [Poly] represents immutable polynomials with integer coefficients. *)
module type Poly = sig
(* [t] is the type of polynomials *)
type t
(* [eval x p] is [p] evaluated at [x].
* example: if [p] represents $3x^3 + x^2 + x$, then
* [eval 10 p] is [3110]. *)
val eval : int -> t -> int
end
```
(The use of `$` above comes from LaTeX, in which mathematical formulas are
surrounded by dollar signs. Similarly, `^` represents exponentiation
in LaTeX.)
##### Exercise: poly spec [✭✭✭]
Finish the design of `Poly` by adding more operations to the interface.
Consider what operations would be useful to a client of the abstraction:
* How would they create polynomials?
* How would they combine polynomials to get new polynomials?
* How would they query a polynomial to find out what
it represents?
Write specification comments for the operations that you invent. Keep
in mind the spec game as you write them: could a devious implementer
subvert your intentions?
□
##### Exercise: poly impl [✭✭✭]
Implement your specification of `Poly`. As part of your implementation,
you will need to choose a representation type `t`. *Hint: recalling
that our polynomials are dense might guide you in choosing a
representation type that makes for an easier implementation.*
□