# The Specification Game

When evaluating specifications, it can be useful to imagine that a game is being played between two people: a specifier and a devious programmer.

Suppose that the specifier writes the following specification:

(** 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 specifier, upon realizing this, refines the spec as follows:

(** [reverse lst] returns a list that is the same length as [lst] *)
val reverse : 'a list -> 'a list


But the devious specifier discovers that the spec still allows broken implementations:

# reverse [1;2;3];;
- : int list = [0;0;0]


Finally, the specifier settles on a third spec:

(** [reverse lst] returns a list [m] satisfying the following conditions:
- [length lst = length m]
- for all [i], [nth m i = nth lst (n - i - 1)],
where [n] is the length of [lst] *)
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 specifier has successfully written her spec.