# Specification
Today we will practice 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 [15 min]
Pair up with another student to play the following game. 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]. For example, if [p] represents
* $3x^3 + x^2 + x$, then evaluating [p] at [10] would yield [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 [10 min]
*Continue to pair up with an other student. Write out your answer to this
exercise on paper, because you're going to share it with another
pair of students when you're done...*
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 [15 min]
Swap your `Poly` specification with another pair of students.
In OCaml, actually code up an implementation of the specification you
just received, or at least as much as you can in the time allotted.
Do your best to implement what you think the specifiers had in mind
(so you don't need to be devious here), but keep notes on what you
found confusing or ambiguous about their specification.
As part of your implementation, you will need to choose a representation
type `t`. Document the abstraction function you choose for that type
as one of your very first activities. *Hint: recalling that our polynomials
are dense might guide you in choosing a representation type that makes for
an easier implementation.*
□
##### Exercise: poly redux [10 min]
Show the other pair of students your implementation of their
specification. Also (politely! non-judgmentally!) tell them about what
you found confusing or ambiguous in their specification. Talk about
what parts were difficult to implement. Discuss which operations are
valuable to have in the signature, and which might be removed. Reflect
on whether there is anything that surprises you in the way the other
team implemented your spec.
□