## 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.ts. 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 TESTs for your is_sorted, max, and sort specifications.