## Representation Invariants and Abstraction Functions Review the [stack and queue code](../08-modules/code.ml) that accompanies the modules lecture. Each of the 4 modules defines an abstract data type. **Exercise**: The two Queue implementations document the abstraction function and rep. invariants, but these are not clearly identified as such. Modify the comments to identify the abstraction functions and rep. invariants (if any). **Exercise**: Describe the abstraction functions and rep. invariants (if any) for the two Stack implementations. **Exercise**: Write a `rep_ok` function for the `TwoListQueue` module. Modify the public functions so that they check `rep_ok` before returning. ## The specification game 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: ``` utop# 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: ``` utop# 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. **Partner exercise**: This example can be made into a 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 a partner to write precise specifications for the following functions (alternate who goes first): - `is_sorted : 'a list -> bool` - `sort : 'a list -> 'a list` - `max : 'a list -> 'a` ## Specification tests Precise specifications for functions can be tested for any particular input. For example, here is the spec we wrote for `reverse` above: ``` (** 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 ``` And here is some code to test it: ``` (** range i n outputs the list [i; i+1; ...; n] *) let rec range i n = if i >= n then [] else i::(range (i+1) n) (** check_reverse_spec l returns true if reverse implements its spec on input l. *) let check_reverse_spec l = let open List in let m = reverse l in length l = length m && let n = length l in for_all (fun i -> nth m i = nth l (n - i - 1)) (range 0 n) ``` **Exercise**: write a similar function for your specification for `is_sorted`, `max`, and `sort`. These functions will check that the function has the correct behavior on any given input. To turn them into tests, you can simply run them on a list of example inputs: ``` TEST "reverse spec" = List.for_all check_reverse_spec [[1;2;3]; []; [1]; [2;2;2;3;3;3]];; TEST "sort_spec" = List.for_all check_sort_spec [[1;2;3]; []; [1]; [2;2;2;3;3;3]];; ``` ### Quick check For some data types, coming up with a good list of examples to use as tests can be difficult. An alternative approach is use randomized tests. The `qcheck` library makes this fairly easy. The `Assertions` module (which is part of the cs3110 tools) contains the `assert_qcheck` function: ``` val assert_qcheck : 'a QCheck.Arbitrary.t -> ('a -> bool) -> unit ``` The first argument is an `'a QCheck.Arbitrary.t`, which gives a way to generate a random value of type `'a` (more on this type below). The second argument is a test function, something like `check_reverse_spec` above. `assert_qcheck` will generate a large number of tests, and check the property on all of them. If any of them fail, it will raise an exception that contains the failing instances. You typically use `assert_qcheck` with `TEST_UNIT`, like so: ``` TEST_UNIT "reverse spec" = Assertions.assert_qcheck arbitrary_list check_reverse_spec ``` How does one create an `'a QCheck.Arbitrary.t`? The [QCheck.Arbitrary](http://cedeela.fr/~simon/software/qcheck/QCheck.Arbitrary.html) module contains a large number of functions for building `Arbitrary.t`s. For example: - `Arbitrary.alpha` is a `char Arbitrary.t`: it generates a random alphabetic character. - `Arbitrary.int n` is a `int Arbitrary.t`: it generates a random number between `0` and `n`. - `Arbitrary.(n -- m)` is an `int Arbitrary.t`: it generates a random number between `n` and `m` - `Arbitrary.list` takes an `'a Arbitrary.t` and produces an `('a list) Arbitrary.t`. For example, `Arbitrary.(list (40 -- 100))` generates a random list of numbers, each between 40 and 100. `Arbitrary.(list alpha)` generates a random list of characters. - `Arbitrary.pair` takes two arbitrary values and generates an arbitrary pair of values. For example, `Arbitrary.(pair (0 -- 100) alpha)` generates pairs where the first element is a number between 0 and 100, and the second element is a character. **Exercise**: Give a value of type `((int * (char list)) list * bool) Arbitrary.t`: ``` open QCheck let arbitrary_thing : ((int * (char list)) list * int) Arbitrary.t = Arbitrary.( FILL IN ) ``` **Exercise**: Use `assert_qcheck` to write `TEST`s for your `is_sorted`, `max`, and `sort` specifications.