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.