# 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. □