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