Functional Programming and Software Engineering

Specification

Terminology
- Specification: what the program should do
- Implementation: how it does it
Let us step back and look at the bigger picture of specifying

Correctness

The high-level goal is to have software that is correct
There are many levels of interpretation for correct
- Informal spec.: we had some vague idea of what the code should do, wrote it, and iteratively addressed feedback of users until bug reports shrunk to very low levels.
- Semi-formal spec.: Sat down with stakeholders, wrote out a specification document in English with a few pictures/formulas, added many tests to code which affirmed all aspects of this spec.
- Rigorous spec.: Have an unambiguous mathematical notion of what correct behavior should be, write it out as the formal specification, make sure code meets it.
The best mode from the above depends on the project: how complex are the algorithms/architecture, and how mission-critical is it?
- Need to go further down the above list as complexity and mission-critical aspects increase

Forms of specification

Specifications span a big range of detail and completeness

From informal descriptions to completely rigorous and unambiguous definitions
From just specifying a few aspects to specifying the whole behavior.
Requirements and Design documents: high-level informal descriptions of what the app should do
- This is the classic form of specification in software engineering; includes description/pictures/etc but is far from code
Types, e.g. writing an .mli file before implementing the code
- Gives a very rigorous, compiler-checked skeleton for the code; we are doing this for you on the assignments
- Much more precise than design docs in terms of code/spec relationship
- But, limited expressiveness since types can express only so much (no “the tree is balanced” in an OCaml type)
Tests
- A test suite constitutes a specification on a finite window of behavior - can’t run on the unbounded input possibilities
- So, 100% accurate on the cases tested, but could miss many important cases if tests are not thoughtfully written.
- Coverage measurements can be used to improve tests: what lines of code were not reached by any test?
Assertions specifying code behavior in mathematical logic
- Preconditions, postconditions, invariants (more below)
Verified assertions aka formal methods
- Verify the code meets preconditions/postconditions/invariants using a tool (Roq/Lean/Dafne/Z3/etc)
- This is like nuclear fusion: a research topic for 50+ years, slowly becoming more viable.

Type-directed programming

As mentioned above, types are a very lightweight but precise layer of code specification
- Particularly nice in that they are all quickly checked and can even be inferred.
- Think of types as outlining the “shape” of the code you need to write in terms of the data structures/functions.

What is Type-Directed Programming??

In fact, you have been doing type-directed programming all along
- We gave you the types for the HW questions, and those types are useful in writing/debugging your code, right??
That is all the principle is: writing code that matches declared type will get you well on the way to an implementation
- So, type-directed programming means start with the type
- Type errors are definitely errors, no need to run tests to find them, the editor will yell at you immediately.
- When the last type error drops, the code often will directly work
Type-directed programming is 100% rigorous, but is incomplete: types only express rough shapes of data
- e.g. int list is a rough shape compared to “sorted int list” but the latter isn’t a type in OCaml
- Our lab (and others) are working on type systems which allow you to write types like { l : int list | is_sorted(l) }”

Simple type-directed programming examples

Not bubbling up option or other wrapped results properly

# let sum_nth_list (l : int list list) (n : int) : int =
  List.nth_opt l n
  |> List.fold_left (fun acc elt -> acc + elt) 0
;;
Error: This expression has type int list option
       but an expression was expected of type int list

Recall that List.nth_opt doesn’t just return a list, the programmer missed that here.
Instead it returns an option list since the n could have been beyond the end of the list.
To solve this type error you will need to match on the result, which should fix both type error and code behavior.

Variation on type-directed programming: with only some parameters applied, the remaining types hint at what is still needed.

# List.fold_left (fun acc elt -> acc - elt);;
- : int -> int list -> int = <fun>

The type shows that we first need the integer initial value and then the list.
In VSCode you can better see this by hovering over the expression.

The type in an .mli file can direct your implementation, e.g. map on Simpledict example from Assignment 3 (where t here is Simpledict.t):

val map : (string -> 'a -> 'b) -> 'a t -> 'b t

Q: “How can I get a dict of 'b’s built from a dict of 'a’s here?”
A: “Use the function from 'a to 'b to make elements of 'b Simpledict.t.

Variant extension: add a new variant case, chase the type errors to patch the code (similar tactic for record field addition)

type party = Dem | Rep

type voter = { name : string ; party : party }

let count_parties (l : voter list) =
  List.fold_left (fun (cd, cr) { party ; _} ->
    match party with
    | Dem -> (cd + 1, cr)
    | Rep -> (cd, cr + 1)
  ) (0, 0) l
;;

Adding a Gre for green party: first just change the type, and chase/fix errors.

# type party = Dem | Rep | Gre

type voter = { name : string ; party : party }

let count_parties (l : voter list) =
  List.fold_left (fun (cd, cr) { party ; _} ->
    match party with
    | Dem -> (cd + 1, cr)
    | Rep -> (cd, cr + 1)
  ) (0, 0) l
;;

Lines 7-9, characters 4-25:
Warning 8 [partial-match]: this pattern-matching is not exhaustive.
  Here is an example of a case that is not matched: Gre

type party = Dem | Rep | Gre
type voter = { name : string; party : party; }
val count_parties : voter list -> int * int = <fun>

This shows a new match case is needed; in the process of adding new case, it will become clear a triple is also needed.
This example also shows why non-exhaustive pattern matches are bad: errors often lurk.
- This is why polymorphic variants are not typical. They are useful at times, but they do not help you with errors like this.

Conclusion: Do not wrestle with OCaml’s types, dance with them.

Preconditions, Postconditions, and Data Structure Invariants

To make more rigorous specs of code use these

A precondition is a logical constraint on function arguments (before it is called: “pre”)
A postcondition is a constraint on the value returned from a function (after: “post”)
An invariant is a property internal to the function or internal to a data structure that always holds (it “invariably” holds except perhaps in the middle of an update)
- Some examples
  - precondition on a function that tree parameter is a binary search tree (left values < right values)
  - postcondition that List.sort always returns a sorted list
  - precondition/postcondition on a tree add function that if the input tree is a BST the output tree will also be.
  - invariants on internal data structures such as a Set implementation which uses an underlying always-sorted list.
  - inductive invariants on recursive algorithms, e.g. assuming in the body of list reverse that it works on a shorter list.
- Logical assertions are more general than tests since they are for all inputs
  - but not necessarily verified (but, invariants do guide tests - write tests to verify on lots of examples)

Let us consider some preconditions and postconditions on the Simple_set.Make functor example (click for zipfile):

module Make (M : EQ) = struct
  type t = M.t list

  let empty : t = []

  let add (x : M.t) (s : t) : t = x :: s

  let rec remove (x : M.t) (s : t) : t =
    match s with
    | [] -> failwith "item is not in set"
    | hd :: tl -> if M.equal hd x then tl else hd :: remove x tl

  let rec contains (x : M.t) (s : t) : bool =
    match s with
    | [] -> false
    | hd :: tl -> if M.equal x hd then true else contains x tl
end

Here are some pre/post conditions in the above code:

Precondition on remove: s is not empty (fails otherwise).
Stronger precondition on remove: contains x s must hold.
Postcondition on remove for it returning set s': not (contains x s') - ??
- This simple “set” data structure is in fact a multiset and this will not always hold.
- If we were trying to implement a true set, this postcondition would help us catch an error.
Postcondition on add x s: for the resulting set s', contains x s' holds.

Assertions in code

OCaml assert statements can be placed in code to directly verify properties.
- The program will die if the assertion fails, so the assertion should always hold.
- It silently returns () if it succeeds.

Example new version of add above:

let add (x : M.t) (s : t) =
let s' = x :: s in assert (contains x s'); s'

Asserts are handy for development mode, but not after deployment (slows things down).
- The compiler has an option to turn assertions off in release mode: -noassert.
Generally it is better to make tests to spot-check assertions instead of using assert.
- But, one thing handy about assert is it puts the assertions in the code, as “rigorous comments”.
- Middle approach: ppx_inline_tests is a library where you can write tests in-line with your code.
- example:
```
let%test "add adds" = contains (add (add 5 emptyset) 22) 22
```

Data structure invariants

As discussed above, data structure invariants are useful when not all elements of a type are “good” to have around in a context
- for example the BST example mentioned above
Example from simpledict on homework: is_ordered must hold for the Simpletree.t.

Recursion Invariants

Recursion and other loops (e.g. in fold) is a prime place to assert invariants
(Even if you don’t write them out, thinking of the invariants are critical to coding recursive programs)
A standard invariant for recursive functions is that the recursive calls return what the calling function expected

let rec rev l =
  match l with
  | [] -> []
  | x :: xs ->
    let rxs = rev xs in
    assert (List.rev xs = rxs);
    rxs @ [x]

Note that we have to use the built-in List.rev to test our version - somewhat circular
In general, a major issue with specification is it is often very difficult to give a code-based definition of the full spec.
So, the main focus should be on partial specs: use some sanity-check conditions.

Examples of Invariants Over Folds

In re-implementing some of the common List functions with fold_left, it helps to think of the invariant.
Folding left (List.fold_left):
- Suppose we are at some arbitrary point processing the fold;
- assume accumulation acc has “the result of the task” for all elements to the left in the list
- require f to then “do the task” to incorporate the current element elt
- also assume acc is initially init
Folding right: very similar, but acc is result for all elements to the right in the list

(* invariant for length via fold_left: acc is number of elements to the left of the current `elt` we are at *)
let length l =
  List.fold_left (fun acc _ -> acc + 1) 0 l

(* invariant for rev via fold_left: acc is reverse of list up to here *)
let rev l =
  List.fold_left (fun acc elt -> elt :: acc) [] l

(* invariant for map via fold_right: acc is f applied to each element of list after here *)
let map f l =
  List.fold_right (fun elt acc -> f elt :: acc) [] l

(* etc *)
let filter f l =
  List.fold_right (fun elt acc -> if f elt then elt :: acc else acc) [] l

Specification and Abstraction

The more completely a module is specified, the less the users need to know about the underlying implementation.
OCaml’s Map module is an example where the users need to know limited information about the implementation.
- They still do need to know it is O(log n) for add/remove/find, which should be in the docs (.mli/odoc)
On your own libraries, you will want to document them well.
- It will make it a lot easier for your users, they can just think about the spec. view.
- odoc formatting for .mli files is in the FPSE Style Guide

Testing

Writing tests has two important and distinct goals.
1. For specification: use tests to define and refine what the code should do
  - Writing tests before fully coding the answer lets the tests serve as your “coding spec”
  - Adding tests for corner cases will clarify the behavior in those cases
    (e.g. does removing an element from a set which doesn’t contain the element raise an exception, or does it just return the set unchanged?)
2. For implementation: use tests to find bugs in code
  - Before the code is working the tests will point out which cases are failing
  - Adding tests covering past bugs will make sure they are caught quickly next time
  - Related term: regression testing, running tests after an update to make sure your code didn’t regress, i.e. old bugs resurfaced
Related terminology you may see
- Black-box tests are tests written against the spec
- Glass-box tests are in the context of bugs in the code and other code properties

Standard categories of tests

Unit testing: what you have mainly done – test the small pieces of the app; no I/O testing
Acceptance testing: test the bigger pieces including I/O
- For example testing your A4 keywordcount.exe on a certain fixed directory tree.
- We in fact give you an acceptance tester there, exec_tests.ml which tests this executable.
Random testing of which there are many types: fuzz testing / monkey testing / property-based testing / quickcheck:
- the tests are run on data generated randomly from some distribution
- “quickcheck”ing aka property-based testing is running unit tests on randomly generated data (random lists of ints, etc)
- “fuzz testing” is running acceptance tests with random input data supplied.

OUnit2

We have been using the OUnit2 library mostly as a black box up to now
Now we will go through the details, which are in fact very simple
- There is not much in OUnit2 per se, if you want something extra just write some higher-order functions to do it

To review, here is your standard simple tests.ml file, this one is from the String_set example:

open OUnit2
open String_set

let tests =
  "test suite for simple set" >:::
    [ "empty"        >:: (fun _ -> assert_equal empty empty)
    ; "3-elt"        >:: (fun _ -> assert_equal true (contains "5" (add "5" empty)))
    ; "1-elt nested" >:: (fun _ -> assert_equal false (contains "5" (remove "5" (add "5" empty))))
    ]

let () = run_test_tt_main tests

OUnit2.assert_equal is just the OUnit2 version of assert.
- It uses (=) for simplicity (but be careful because as we discussed it is equality of runtime representation, which is usually not the intended notion of equality on Map/Set for example)
The infix >:: operator takes a string (test name) and a piece of test code under fun _ -> (to keep it from running right away) and builds a single test of type test (run #require "ounit2" and open OUnit2 in the top-loop before playing with this code there):
```
# let test1 = "simple test" >:: fun _ -> assert_equal (2 :: []) [2];;
val test1 : test = TestLabel ("simple test", TestCase (Short, <fun>))
```

The >::: operator simply takes a test list and builds a test suite (which in fact is just of type test)

# let test_suite = "suite now" >::: [test1];;
val test_suite : test =
  TestLabel ("suite now",
  TestList [TestLabel ("simple test", TestCase (Short, <fun>))])

Then, OUnit2.run_test_tt_main tests will run the suite tests
- (Note this will work but will then freeze the top loop - OUnit is designed to run in the command line only)

How the tests run when you say dune test

The above tests.ml file is just defining an executable, like keywordcount.exe in Assignment 4.
Build and run the executable to run the tests.
Here is a dune build file which would work for the Simple_set tests, for example:

(executable
 (name tests)
 (libraries
   ounit2
   simple_set
 ))

; dune rule so that command line "dune runtest" (and "dune test") will run tests.
; in other words, there is nothing special about `dune test`. It is just a build plus running `_build/default/test/tests.exe`
(rule
 (alias runtest)
 (action (chdir %{project_root}
  (run ./test/tests.exe))))

There is even special shorthand for the above: replace executable with test and it makes an executable plus the above alias to run tests:

(test
 (name tests)
 (libraries
   ounit2
   simple_set
 ))

Higher-order testing

If you did unit testing in other languages it looks pretty much like the above.
But in OCaml we can make tests programatically which makes for less code duplication.
Example: lets make a bunch of different tests on the same invariant that reversing a list twice is a no-op:

# let make_rev_test l =
  "a rev test" >:: (fun _ -> assert_equal l (List.rev @@ List.rev l))
;;
val make_rev_test : 'a list -> test = <fun>

let make_test_suite l ~f =
  "suite of tests of f" >::: List.map f l
;;
val make_test_suite : 'a list -> f:('a -> test) -> test = <fun>

let s = make_test_suite [[];[1;2;3];[2;44;2];[32;2;3;2;1]] ~f:make_rev_test ;;
let () = run_test_tt_main s;; (* recall this crashes the top loop when finished *)

In general you can build an arbitrarily big tree of tests with suites of suites etc.
- As can be seen above, a suite of tests just has type test

let s' = "id tests" >:::
  [ "one" >:: (fun _ -> assert_equal (Fun.id 4) 4)
  ; "two" >:: (fun _ -> assert_equal (Fun.id "hello") "hello") ]
;;

let suites = test_list [s;s'];; (* make suite of suites *)

let named_suites = "revrev and Fun.id" >: suites (* any tree of tests can be named with >: *)

Here is the type of test under the hood (from the docs) which should make clear why the above works:

type test =
  | TestCase of test_fun
  | TestList of test list
  | TestLabel of string * test

Tangent: defining infix operators

The OUnit infix operators >:/>::/>::: are just like +, ^ etc
Using them arguably makes the code more readable, so consider defining your own infix operators when appropriate.

# #require "ounit2";;

# open OUnit2;;

# (>::) ;;
- : string -> test_fun -> test = <fun>

# (>:::);;
- : string -> test list -> test = <fun>

There is no magic to infix operators like this. You can also do it:

# let (^^) x y = x + y;;
val ( ^^ ) : int -> int -> int = <fun>

# 3 ^^ 5;;
- : int = 8

Note that unlike in C++, we are not overloading operators, ^^ only works on two ints now.
The old version of ^^ for printing is now shadowed so is not directly accessible.
So, new infix ops are always defined within a module to avoid overlap.

The different assert_X statements possible in OUnit2

We used assert_equal above which is the OUnit function to check things being equal
assert_bool is like the assert OCaml command: assert_bool "name that test" (0=0) for example
OUnit2.assert_raises is also often useful, it verifies that an exception is raised when it should be:
```
let atest = fun _ -> assert_raises (Failure "nth") (fun () -> List.nth [1;2;3] 4)
```
To perform acceptance testing (I/O), use assert_command to run a shell command and compare against output
- in the A4 exec_tests.ml code we provided, you can see we are using assert_command to test the executable
If you need fixed setup/teardown code bracketing a group of tests to setup e.g. files: bracket_tmpfile

As always, see the documentation for more details:
OUnit2 API docs

Bisect for OCaml code coverage

Code coverage is a great glass-box (implementation-based) metric of how good your test suite is
The simple idea of coverage: are there lines of your code that never get exercised by any of your tests?
Coverage tools let you easily check this.
We will use the Bisect coverage tool for our OCaml code

Using Bisect

The bisect_ppx preprocessor can decorate your code with one hit-bit per line
- it can then show which lines are “hit” upon running your test suite
It is a pre-process extension (ppx), meant to work as backend instrumentation, not for macro programming like most other ppx.
- e.g. ppx_deriving produces code you actually use. bisect_ppx just affects what happens when your program runs (it counts the lines hit).
Add it as instrumentation with the (instrumentation (backend bisect_ppx_ng)) line to the library or executable declaration in dune.
- Do not to add it to your (test ...) declaration because that would count which lines are hit in your testing code, not your actual code!
- Then, due to some obscure issues involving how dune runs tests there is currently some hacking needed to output the files with the coverage results
  - The tests/dune file needs to be more complex to do this
  - (The reason why is dune now sandboxes test running, they can’t do I/O like writing files without explicit permissions.)
Now test your code while telling dune to instrument so it can track which lines were hit:
```
dune test --instrument-with bisect_ppx_ng
```
Then print the coverage summary:
```
bisect-ppx-report summary
```
or
```
bisect-ppx-report html
```
for a pretty report, found in _coverage/index.html, which you should open with your browser.
See Bisect docs for more details
Note that if you have single lines of code that you know should not be run (e.g. invariants that should not fail) you can put [@coverage off] at the end of those lines. To turn coverage off on a single let definition, put [@@coverage off] immediately after the end of definition. To turn coverage off on an arbitrary range of lines in the file, put [@@@coverage off] to turn it off and then [@@@coverage on] to turn it back on. See the docs for details.

We will check how well my tests of the simple set example covered the code using Bisect.

See the set-example/tests/dune file for the fancy boilerplate you need to add bisect to your project test runner.

Random Testing aka Property-Based Testing aka Quickchecking

Recall that Quickchecking is making up some random data to test our code
To use random testing we need to know when the code is “working” on that random data
- e.g. add a bunch of random key-value maps to a dictionary and delete them: should be the original dictionary again
- e.g. above of reversing a reversed list gives back the original (randomly generated) list
- So, its better for testing invariants on data structures and functions
- But it can also hit corner cases, e.g. empty list case not properly handled etc.

Here is the methodology

Given: a function f that we want to test.
Have a function to generate random data which is the parameters of f
Run f on that random data many times (say 1000 times)
Verify whether the test “worked” on that random data

Using `QCheck`

For step 1. above we want to not have to “roll our own” every time
QCheck is a library that will do it for us
QCheck contains three key algorithms:
1. Gen, QCheck.Gen - make random data of desired distribution in given type
2. Shrinkers, QCheck.Shrink - if a failing case is discovered, try to make random data smaller, e.g. a shorter list (note we will not cover shrinkers in detail)
3. Maker, QCheck.Test.make which makes a test over the random data
4. Runner, QCheck.Test.check_exn, which runs some fixed number of random tests and shrinks failures.
We will look at several examples of the QCheck library in action in quickcheck_examples.ml/quickcheck_examples.zip
We will look at quickchecking on a Map in school_qcheck.ml/school_qcheck.zip
QCheck docs

Fuzz testing vs Quickcheck

Fuzz testing aka fuzzing is to acceptance tests as quickcheck is to unit tests
- fuzzers feed random inputs into an app to see what it does (acceptance test modality)
- quickcheckers on the other hand are testing single functions (unit test modality)
Industry fuzz testers do a lot more more than generate totally random data
- They may be aware that the string input should fit a particular grammar, e.g. html
- They may be combined with a coverage tool and work to find random data inputs covering all the code

FPSE