< 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.
]]>