1.6.1. Exercise 1¶
Give an example of a real-life application that requires an implementation of and algorithm (or several algorithms) as its part, and discuss the algorithms involved: how do they interact, what are they inputs and outputs.
1.6.2. Exercise 2¶
Programming in OCaml in Emacs is much more pleasant with instant navigation, auto-completion and type information available. Install all the necessary sofwtare following the provided Software Prerequisites.
1.6.3. Exercise 3¶
What is the termination measure of
Define it as a function
f : 'a list -> int -> int and change the
walk annotating it with outputs to check that
the measure indeed decreases.
- Hint: use OCaml’s
Printf.printfutility to output results of the termination measure mid-execution.
1.6.4. Exercise 4¶
Implement the function
find_min2, similar to
find_min(also using the auxiliary
walk, but without relying on any other auxiliary functions, e.g., sorting) that finds not the minimal element, but the second minimal element. For instance, it should bive the following output on a list
[2; 6; 78; 2; 5; 3; 1]:
# find_min2 [2; 6; 78; 2; 5; 3; 1];; - : int option = Some 2
walkis easier to implement if it takes both the “absolute” minimum
m1and the second minimum
m2, i.e., has the type
int list -> int -> int -> int.
Write its specification (a relation between its input/output).
Hint: the following definition might be helpful:
let is_min2 ls m1 m2 = m1 < m2 && List.for_all (fun e -> e == m1 || m2 <= e) ls && List.mem m2 ls
Write the precondition for
walkand annotate the function with the assertions, enforcing the pre- and postconditions.
Hint: you might want to start from devising the second disjunct of
find_min2_walk_pre ls xs m1 m2to state that “a list has an element that is its second minimum, positioned appropriately with respect to
Test your annotated function
1.6.5. Exercise 5¶
Give an example of an interesting non-tail recursive function in OCaml and show, if possible, an equivalent tail-recursive function.
1.6.6. Exercise 6¶
Implement an imperative version of the function
Exercise 4, annotate its with loop invariants and run
1.6.7. Exercise 7¶
Implement a version of an insertion sort that sorts the elements in the descending order and test it.
1.6.8. Exercise 8¶
It is possible to implement (quite unelegantly and not very
efficiently) the insertion sort on lists, so it would be
tail-recursive. For this, we will have to rewrite it, so
would use the boolean flug
run in order to indicate whether the
insertion has already taken place, or the iteration should continue:
let insert_sort_tail ls = let rec walk xs prefix = match xs with |  -> prefix | h :: t -> let rec insert elem acc remaining run = if not run then acc else match remaining with |  -> acc @ [elem] | h :: t as l -> if h < elem then let run' = true in let acc' = acc @ [h] in insert elem acc' t run' else let run' = false in let acc' = acc @ (elem :: l) in insert elem acc' t run' in let acc' = insert h  prefix true in walk t acc' in walk ls 
Define the invariants for auxiliary functions:
let insert_inv prefix elem acc remaining run = (* ... *) let insert_sort_tail_walk_inv ls xs acc = (* ... *)
Annotate the implementation above with them and test it.
insert_sort_tailinto an imperative version, which uses (nested) loops instead of recursion.