Lecture 9 — Code validation: from specifications to tests

The question

How can code quality be assured based on specifications?

Since week 2 we have written specifications without calling them that: the val lines F# Interactive prints, the "e.g. … should return" lines of every homework, Lecture 5's "a type is a promise", Lecture 8's equations such as factA n acc = acc * fact n. Lecture 8 derived code from a specification. Today we go the other way: the code is given, and we check it against the specification.

Plan: (1) a specification says what; (2) the module boundary; (3) unit tests — NuGet, fixtures, runners; (4) properties and models; (5) the map of testing techniques, and the answer to the question.

1 · A specification says what

A specification says what the code must do; validation compares the code with it.

A specification is independent of how the code does it. We have used three forms all semester.

Three forms you have already used

A type is a specification: val insert: x: 'a -> t: 'a BinTree -> 'a BinTree when 'a: comparison (Lecture 6) promises a tree back for every value and every tree, and rules out everything else ("a type is a promise", Lecture 5). The compiler checks it.

An example is a specification: "contains 13 t should return true" (the shape of every "e.g." line in a homework). A test checks it.

An equation or an invariant is a specification: factA n acc = acc * fact n (Lecture 8), or "the in-order list of a search tree is sorted" (Lecture 6). It says something about all inputs at once.

Which form is it?

Five fragments; for each, say which form it is and what could check it. The answers are at the end of this section.

1. val insert: x: 'a -> t: 'a BinTree -> 'a BinTree when 'a: comparison
2. "contains 13 t should return true"
3. factA n acc = acc * fact n
4. "the in-order list of a search tree is sorted"
5. "insert does the same as Set.add on the in-order list"

A check on a point

Here is a factorial with a "special case" (the opening of the 2025 lecture on property-based testing):

let rec fact n =
  match n with
  | 0 -> 1
  | 7 -> fact 6
  | n -> n * fact (n - 1)

A plain check compares an expected value with an actual one:

let check name expected actual =
  if expected = actual then true
  else failwith $"check failed: {name}"

let fact0 = check "fact 0" 1 (fact 0)
let fact3 = check "fact 3" 6 (fact 3)
let fact5 = check "fact 5" 120 (fact 5)

true

true

true

Three checks pass. Is fact correct? What is fact 7?

let fact7 = fact 7

720

The specification "fact n = n * fact (n - 1) for every n > 0" fails at 7:

let factEquation = List.forall (fun n -> fact n = n * fact (n - 1)) [1 .. 10]
let factCounterexample = List.tryFind (fun n -> fact n <> n * fact (n - 1)) [1 .. 10]

false

Some 7

A check on a point says nothing about the other points. The equation speaks about all of them; the question of this lecture is how to check that.

Answers: which form is it?

1. A type — checked by the compiler, for every input, before the program runs.
2. An example — checked by a unit test (concept 3).
3. An equation — checked by a property test over many inputs (concept 4), or by a derivation as in Lecture 8.
4. An invariant — checked by a property test over many trees, or enforced at a module boundary so that no tree can violate it (concept 2).
5. A model — checked by comparing the code with the simpler implementation on the same inputs (concept 4).

Why it matters: without a specification there is nothing to check against. Every technique on today's map starts from one of these forms.

2 · The module boundary

A module boundary is where a specification is enforced: what a client cannot see, a client cannot break.

From Lecture 6

The binary tree, the search-tree functions and the two example trees:

type 'a BinTree = Empty
                | Node of 'a BinTree * 'a * 'a BinTree

let leaf x = Node (Empty, x, Empty)

let t = Node (Node (leaf 2, 7, Empty),
              9,
              Node (leaf 13, 21, leaf 25))

let rec insert x t =
  match t with
  | Empty -> Node (Empty, x, Empty)
  | Node (l, y, r) ->
      match compare x y with
      | 0 -> t
      | c when c < 0 -> Node (insert x l, y, r)
      | _ -> Node (l, y, insert x r)

let rec contains x t =
  match t with
  | Empty -> false
  | Node (l, y, r) ->
      if   x < y then contains x l
      elif x > y then contains x r
      else true

let rec inOrder t =
  match t with
  | Empty -> []
  | Node (l, x, r) ->
      inOrder l @ [x] @ inOrder r

let bad = Node (leaf 5, 3, Empty)

And bad:

The search-tree invariant (Lecture 6): for every Node (l, x, r), every value in l is less than x and every value in r is greater. t satisfies it; bad does not, and the type does not care.

What is inOrder (insert 4 bad)?

let inOrderBad4 = inOrder (insert 4 bad)

[5; 3; 4]

Garbage in, garbage out

Not sorted. The tree insert 4 bad:

insert preserves the invariant, but nothing stops a client from writing Node (leaf 5, 3, Empty) and handing it to insert. A predicate states the invariant:

let isSearchTree t =
  let xs = inOrder t
  xs = List.sort xs && xs = List.distinct xs

let isSearchTreeT = isSearchTree t
let isSearchTreeBad = isSearchTree bad

true

false

What would keep the invariant? Make it impossible to build a tree except through insert. That needs a boundary.

Modules

Every script and every file is a module: Lecture 2 said that a let at the top of a script defines a value "at the toplevel of the module". A module can also be declared inside a script:

module Greeting =
  let private prefix = "Tere, "
  let greet name = prefix + name + "!"

let greeting1 = Greeting.greet "Mari"

"Tere, Mari!"

A module's members are used with the module's name in front, or after open:

open Greeting
let greeting2 = greet "Jaan"

"Tere, Jaan!"

prefix is private: visible inside Greeting, invisible outside it.

> Greeting.prefix;;
error FS1094: The value 'prefix' is not accessible from this code location

Qualified access

Lecture 5 used Set.add, Map.find, List.map — never open Set. The library marks those modules so that their short names cannot flood a script:

[<RequireQualifiedAccess>]
module Temperature =
  let freezing = 0.0
  let toFahrenheit c = c * 9.0 / 5.0 + 32.0

let boiling = Temperature.toFahrenheit 100.0

212.0

> open Temperature;;
error FS0892: This declaration opens the
module 'FSI_0001.Temperature', which is
marked as 'RequireQualifiedAccess'. Adjust your code to use qualified
references to the elements of the module instead, e.g. 'List.map'
instead of 'map'. This change will ensure that your code is robust as
new constructs are added to libraries.

A search tree module

A search tree is a binary tree that was built by insert only. The module wraps Lecture 6's tree in a one-case union whose case is private — Lecture 7's trick for the email address:

[<RequireQualifiedAccess>]
module SearchTree =
  type 'a SearchTree when 'a : comparison =
    private ST of 'a BinTree
  let empty = ST Empty
  let insert x (ST t) = ST (insert x t)
  let contains x (ST t) = contains x t
  let toList (ST t) = inOrder t

The insert on the right-hand side is Lecture 6's. The module's own insert is not in scope until its definition is complete.

let st =
  SearchTree.insert 4
    (SearchTree.insert 9
      (SearchTree.insert 7 SearchTree.empty))

let stList = SearchTree.toList st

[4; 7; 9]

What can a client do?

Build the tree bad through the module?

> let bad' = SearchTree.ST (Node (leaf 5, 3, Empty));;
error FS1093: The union cases or fields of the type 'SearchTree' are not
accessible from this code location

Only empty and insert build a search tree, and insert preserves the invariant, so every 'a SearchTree satisfies it. The invariant has become a promise of the type: the boundary enforces the specification.

What can a test of the module call? Only what the module exports: empty, insert, contains, toList. A test is written against the specification, not against the representation, and survives a change of representation.

Files are modules

A file SearchTree.fs that starts with module SearchTree is the same module as a file. A script loads it with #load:

> #load "SearchTree.fs";;

A file sees only the files loaded before it. Loading a client before the module it uses fails:

> #load "Client.fs" "SearchTree.fsi" "SearchTree.fs";;
Client.fs(3,13): error FS0039: The value, namespace, type or module
'SearchTree' is not defined.

There are no cycles between files; a project lists its files in the same order, and the rule is the same. Several files can share a namespace, a name for a group of modules and types:

namespace Itt8060.Lecture9

module SearchTree =
  ...

type Direction = Left | Right

A script cannot declare a namespace; a file in a project can.

The signature file

A signature file SearchTree.fsi is the interface written down: the val lines F# Interactive has been printing all semester, and the types, with the representation left out.

module SearchTree

type 'a SearchTree when 'a : comparison

val empty : 'a SearchTree
val insert : 'a -> 'a SearchTree -> 'a SearchTree when 'a : comparison
val contains : 'a -> 'a SearchTree -> bool when 'a : comparison
val toList : 'a SearchTree -> 'a list

The signature is loaded before the implementation:

> #load "SearchTree.fsi" "SearchTree.fs";;
[Loading .../SearchTree.fsi
 Loading .../SearchTree.fs]
module FSI_0002.SearchTree
...
val empty: 'a SearchTree when 'a: comparison
val insert: x: 'a -> 'a SearchTree -> 'a SearchTree when 'a: comparison
val contains: x: 'a -> 'a SearchTree -> bool when 'a: comparison
val toList: 'a SearchTree -> 'a list when 'a: comparison

> SearchTree.toList (SearchTree.insert 3 (SearchTree.insert 1 SearchTree.empty));;
val it: int list = [1; 3]

The compiler checks the signature

Declare val size : 'a SearchTree -> int in the signature without implementing it:

SearchTree.fs(1,8): error FS0193: Module 'FSI_0001.SearchTree' requires a value 'size'

And the constructor is not merely private; for a client it does not exist:

> let bad' = SearchTree.ST (SearchTree.Node (SearchTree.Empty, 1, SearchTree.Empty));;
error FS0039: The value, constructor, namespace or type 'ST' is not defined.

The complete SearchTree.fsi and SearchTree.fs are in the worked examples.

Why it matters: a specification that a client can bypass is a comment. A specification behind a module boundary is a guarantee, and tests of the module test the guarantee.

3 · Unit tests

A unit test makes one example of the specification executable.

A plain check

We already have one: check from concept 1.

let check13 = check "contains 13 t" true (contains 13 t)
let check8 = check "contains 8 t" false (contains 8 t)
let checkInOrder = check "inOrder" [2; 7; 9; 13; 21; 25] (inOrder t)

true

true

true

This is exactly what the hidden checks of these notes' exercises do: a reference implementation is applied to the stated examples, and a mismatch stops the build. What is missing for a suite of tests: a name for each test, a report that lists them, and a way to run all of them with one command. A library provides that.

NuGet: where libraries come from

A library is a package on nuget.org: a name and a version. A script asks for it with a directive at its top:

#r "nuget: NUnit, 4.3.2"

The first time, F# Interactive fetches the package over the network into the local package cache (~/.nuget/packages) and prints what it loaded:

> #r "nuget: NUnit, 4.3.2";;
[Loading C:\Users\juhan\.packagemanagement\nuget\Cache\0793...e460d.fsx]
module FSI_0002.0793...e460d

Every later run uses the cache and needs no network. Then open NUnit.Framework, and the API from the package's documentation: Assert.That (actual, Is.EqualTo expected), Is.True, Is.Empty.

NuGet: caveats

What does #r "nuget: NUnit", with no version, fetch?

> #r "nuget: NUnit";;
[Loading ...\nuget\Projects\38696--c955...382b\Project.fsproj.fsx]
module FSI_0002.Project.fsproj

> typeof<NUnit.Framework.TestAttribute>.Assembly.GetName().Version;;
val it: System.Version = 5.0.0.0 {...}

The newest release, on the day it was run (2026-10-28). Next month it may be another one, with another behaviour, so a script that others will run pins its version. This lecture pins 4.3.2, the version the .NET 10 SDK's own test template uses.

A package brings its dependencies with it: the cache of the run above also holds fsharp.core 10.1.302, which NUnit's F# support needs. A project lists the same packages as package references in its project file, restored by dotnet restore; we come back to it below.

A fixture

The tests of the search-tree module, in the shape the course's automated tests have. A test script loads NUnit and the module, then declares a fixture: a type whose members are the tests.

#r "nuget: NUnit, 4.3.2"
#load "SearchTree.fsi" "SearchTree.fs"

open NUnit.Framework

let ofList xs =
  List.fold (fun s x -> SearchTree.insert x s) SearchTree.empty xs

[<TestFixture>]
type SearchTreeTests () =
  [<Test>]
  member this.``toList empty is []`` () =
    Assert.That (SearchTree.toList (ofList ([]: int list)), Is.Empty)
  [<Test>]
  member this.``insert keeps the in-order list sorted`` () =
    let t = ofList [3; 1; 4; 1; 5]
    Assert.That (SearchTree.toList t, Is.EqualTo<int list> [1; 3; 4; 5])

A third test, contains finds an inserted value, is in the complete script in the worked examples.

Arrange, act, assert

Each test has three parts: arrange the input (let t = ofList ...), act (SearchTree.toList t), assert one thing about the result (Assert.That (..., Is.EqualTo ...)). One assertion per test, so that a failure names one broken promise.

A test's name is a sentence of the specification, written between double backticks so that it may contain spaces: insert keeps the in-order list sorted. The report lists the names, so the report reads as the specification.

The [<Test>] attribute marks a member as a test; [<TestFixture>] marks the type as a group of tests. NUnit also accepts top-level [<Test>] let functions (the 2025 lecture used them).

Is.EqualTo<int list>: NUnit has three EqualTo overloads, and for an F# list the compiler cannot choose between "a value" and "a sequence", so the type argument says which. For numbers and strings Is.EqualTo 120 is enough.

Running a test is calling it

Load the script in F# Interactive. A loaded script is a module named after the file, so its fixture is Tests.SearchTreeTests:

> #load "Tests.fsx";;
...
> open Tests;;
> SearchTreeTests().``toList empty is []`` ();;
val it: unit = ()

A test is a function. It returns () when the assertion holds and raises an exception when it does not — that is all there is to it.

How a runner works

A test runner finds the tests and calls them. One fits in twelve lines (the end of Tests.fsx):

open System.Reflection

let runTests (asm: Assembly) =
  for fixture in asm.GetTypes () do
    if fixture.IsDefined typeof<TestFixtureAttribute> then
      let instance = System.Activator.CreateInstance fixture
      for test in fixture.GetMethods () do
        if test.IsDefined typeof<TestAttribute> then
          try
            test.Invoke (instance, [||]) |> ignore
            printfn "PASSED  %s" test.Name
          with e ->
            printfn "FAILED  %s\n%s" test.Name e.InnerException.Message

runTests typeof<SearchTreeTests>.Assembly

The attributes are for discovery: every type marked [<TestFixture>], every method marked [<Test>]. Each test is invoked; an exception means a failure. (InnerException: reflection wraps the exception the test raised.)

Running them all

> dotnet fsi Tests.fsx
PASSED  toList empty is []
PASSED  insert keeps the in-order list sorted
PASSED  contains finds an inserted value

What does the runner print for a fixture that tests fact at 0, 3, 5 and 7?

> dotnet fsi FactTests.fsx
PASSED  fact 0 is 1
PASSED  fact 3 is 6
PASSED  fact 5 is 120
FAILED  fact 7 is 5040
  Assert.That(, )
  Expected: 5040
  But was:  720

The message is NUnit's: the test's name, the expected value and the actual one. (The empty Assert.That(, ) is the place where NUnit prints the source text of the assertion; F# does not supply it.)

What the real runner adds

Our runner lacks what NUnit's own runner has:

• Isolation: NUnit records failures in a context that our runner never resets. Call the failing test by hand after the run above and the message lists the failure twice:

  > FactTests().``fact 7 is 5040`` ();; NUnit.Framework.AssertionException: Multiple failures or warnings in test: 1) Assert.That(, ) Expected: 5040 But was: 720 2) ...

• Time limits: a test that loops forever hangs our runner.

• Parallel runs and a report in a standard format.

NUnit's runner cannot run a script's fixtures directly (a script has no assembly file), which is why the course's grader compiles its test scripts first. The usual way to get the real runner is a project.

The same tests in a project

> dotnet new nunit -lang F# -o SearchTree.Tests

The template creates a project file. The module, its signature and the fixture (the same fixture, under module Tests, without the runner) are listed as compile items, in order:

<ItemGroup>
  <Compile Include="SearchTree.fsi" />
  <Compile Include="SearchTree.fs" />
  <Compile Include="Tests.fs" />
  <Compile Include="Program.fs" />
</ItemGroup>

<ItemGroup>
  <PackageReference Include="Microsoft.NET.Test.Sdk" Version="17.14.0" />
  <PackageReference Include="NUnit" Version="4.3.2" />
  <PackageReference Include="NUnit3TestAdapter" Version="5.0.0" />
  ...
</ItemGroup>

The package references are NuGet again: the framework (NUnit), the adapter that lets dotnet test find the tests, and the test host. dotnet test restores them, builds and runs:

> dotnet test
...
Passed!  - Failed:     0, Passed:     3, Skipped:     0, Total:     3, Duration: 19 ms - SearchTree.Tests.dll (net10.0)

The complete project is in the worked examples.

How your homework is graded

The automated tests of this course work the same way, in scripts:

1. Your submitted script is copied under a fixed name and loaded as a module, as SearchTree.fs was.
2. One fixture per task holds the tests of that task's clauses, named as the clauses are; the names you see in the report are the fixture members' names.
3. A task's grade is the share of its tests that pass.
4. Each test has a time limit, so a function that loops forever fails instead of hanging the run.
5. Some of the tests are property-based tests, whose inputs a tool chooses — next week.

What a test cannot tell

fact passed its tests at 0, 3 and 5 and was wrong at 7. A passing unit test says nothing about the inputs it did not use. Tests check examples; the specification speaks about every input. Concept 4 closes the gap from the other side.

Why it matters: a unit test is the cheapest executable specification there is — a name, an input, an expected value — and a runner makes a hundred of them one command.

4 · Properties and models

Properties and models cover inputs you did not think of; a tool can choose the inputs.

The "oracle" problem

Every check needs an expected result — an "oracle" that knows the answer. There are three ways to get one:

• An example: you compute the expected value by hand (fact 5 is 120). Cheap, and limited to the inputs you thought of.
• A property: a relation that holds without knowing the result (fact n = n * fact (n - 1); rev (rev xs) = xs). It can be checked on any input, including inputs a tool chooses.
• A model: a simpler implementation that computes the expected result (Set.add for insert). Slow or naive is fine; it only has to be right.

Properties are equations

A helper checks a property over a list of inputs:

let forAll inputs p = List.forall p inputs

let revPairs =
  [ ([], []); ([1], [2])
    ([1; 2], [3]); ([1; 2; 3], [4; 5]) ]

Does rev (xs @ ys) = rev xs @ rev ys hold?

let wrongRevEquation =
  forAll revPairs (fun (xs, ys) ->
    List.rev (xs @ ys) = List.rev xs @ List.rev ys)

let wrongRevCounterexample =
  List.tryFind (fun (xs, ys) ->
    List.rev (xs @ ys) <> List.rev xs @ List.rev ys) revPairs

false

Some ([1], [2])

No: reversing swaps the halves. rev (xs @ ys) = rev ys @ rev xs:

let rightRevEquation =
  forAll revPairs (fun (xs, ys) ->
    List.rev (xs @ ys) = List.rev ys @ List.rev xs)

true

The fact equation over 1 .. 10, the way concept 1 checked it:

let factEquationHolds = forAll [1 .. 10] (fun n -> fact n = n * fact (n - 1))

false

false, with the counterexample 7 found above. A property is a specification; checking it over inputs is a test of the specification itself, on as many inputs as we care to supply.

A model as the oracle

A search tree is a set, so Lecture 5's Set is the model: insert should do to the in-order list what Set.add does to the set.

let modelInsert x xs = Set.toList (Set.add x (Set.ofList xs))

let build xs = List.fold (fun acc x -> insert x acc) Empty xs

let trees =
  [ build []; build [5]; build [3; 1; 4; 1; 5]
    build [9; 7; 2; 21; 13; 25]; build [1 .. 10] ]

Does inOrder (insert x t) = modelInsert x (inOrder t) hold for these trees and for x in 0, 4, 11?

let modelEquation =
  forAll trees (fun t ->
    forAll [0; 4; 11] (fun x ->
      inOrder (insert x t) = modelInsert x (inOrder t)))

true

The model gives the expected result for every input, so a test of insert no longer needs a hand-computed answer. The same check through the module's SearchTree.toList and SearchTree.insert is a test of the boundary of concept 2.

Next week, and the week after that

Both checks above used inputs we wrote by hand. Two techniques let a tool choose them:

• Property-based testing: a generator produces inputs of the required type, the property is checked on each, and a failing input is "shrunk" to a smallest one that still fails. The tool in F# is FsCheck; next week.
• Model-based testing: the specification is a model (a state machine or a reference implementation); a tool generates sequences of operations, runs them on the code and on the model, and compares. It finds wrong orders of operations, not just wrong values.

Why it matters: a property or a model is a specification that any number of inputs can be checked against. A tool can then supply the inputs you did not think of.

5 · The map

Each technique checks one form of specification over one part of the input space; quality is assured by choosing them together.

The map of testing techniques

Three more rows that do not fit the lecture: code review (the specification is in a colleague's head; finds what no test was written for; cannot find what the reviewer does not read); mutation testing (changes the code on purpose and asks whether the tests notice: a measure of the tests, not of the code); fuzzing (random inputs with no specification but "does not crash").

Where does it go?

Five checks; place each on the map. Answers follow.

1. A val line that does not compile.
2. check "fact 3" 6 (fact 3).
3. forAll inputs (fun xs -> List.rev (List.rev xs) = xs).
4. SearchTree.insert compared with Set.add over sequences of inserts and removals.
5. A "smart constructor" that returns Error for a malformed email address (Lecture 7).

Answers: (1) type checking — the specification is a type, the compiler chose every input; (2) a unit test — an example, you chose the input; (3) a property-based test — an equation, over inputs a tool can choose; (4) a model-based test — a model, over sequences of operations; (5) a runtime check — an invariant, checked on the inputs the real users supply.

The answer

How can code quality be assured based on specifications?

1. Write the specification in a checkable form: a type, an example, an equation, an invariant, a model.
2. Put it behind a module boundary, so that the implementation can change while the specification holds.
3. Execute it, repeatedly, by machine — the runner in your script, the course's pipeline — so that every change is checked again.
4. Choose the technique by the form of the specification and the size of the input space; no single technique covers the map.

Summary

1. A specification says what the code must do; validation compares the code with it.
2. A module boundary is where a specification is enforced: what a client cannot see, a client cannot break.
3. A unit test makes one example of the specification executable.
4. Properties and models cover inputs you did not think of; a tool can choose the inputs.
5. Each technique checks one form of specification over one part of the input space; quality is assured by choosing them together.

Other tools you will meet

• FsUnit: assertion syntax that reads as a sentence on top of NUnit, actual |> should equal expected. Its release must match the NUnit version (FsUnit 8 needs NUnit 5, so it does not pair with the 4.3.2 pinned here).
• Expecto: an F#-native framework; tests are values, testCase "name" <| fun () -> ..., grouped in lists and run from a script or a console program, with no attributes.
• xUnit: the other common .NET framework; [<Fact>] in place of [<Test>], and dotnet new xunit as its template.
• FsCheck: property-based testing — next week.

The course's own tests use NUnit, so NUnit is what you need in order to read your results.

Homework, reading and next week

Homework 6 continues; its defence is next week.

Reading: Hansen & Rischel, Functional Programming Using F#, chapter 7, "Modules" (a fast reading suffices); the F# language reference pages Modules, Namespaces, Signatures and Package references in F# Interactive; the NUnit documentation.

Next week: property-based testing — a tool chooses the inputs.

Worked examples

The complete module, signature and test script of concept 3, and Hansen's vector module. Put the files in one directory and run dotnet fsi Tests.fsx.

SearchTree.fsi

module SearchTree

// The signature: what a client can see and use. The representation of a
// search tree is not declared here, so a client cannot build one by hand.
type 'a SearchTree when 'a : comparison

val empty : 'a SearchTree
val insert : 'a -> 'a SearchTree -> 'a SearchTree when 'a : comparison
val contains : 'a -> 'a SearchTree -> bool when 'a : comparison
val toList : 'a SearchTree -> 'a list

SearchTree.fs

module SearchTree

// Lecture 6's binary tree and its search-tree functions, unchanged.
type private 'a BinTree = Empty
                        | Node of 'a BinTree * 'a * 'a BinTree

module private Tree =
  let rec insert x t =
    match t with
    | Empty -> Node (Empty, x, Empty)
    | Node (l, y, r) ->
        match compare x y with
        | 0 -> t
        | c when c < 0 -> Node (insert x l, y, r)
        | _ -> Node (l, y, insert x r)

  let rec contains x t =
    match t with
    | Empty -> false
    | Node (l, y, r) ->
        if   x < y then contains x l
        elif x > y then contains x r
        else true

  let rec inOrder t =
    match t with
    | Empty -> []
    | Node (l, x, r) ->
        inOrder l @ [x] @ inOrder r

// A search tree is a binary tree that was built by insert only.
type 'a SearchTree when 'a : comparison = private ST of 'a BinTree

let empty = ST Empty
let insert x (ST t) = ST (Tree.insert x t)
let contains x (ST t) = Tree.contains x t
let toList (ST t) = Tree.inOrder t

Tests.fsx

#r "nuget: NUnit, 4.3.2"
#load "SearchTree.fsi" "SearchTree.fs"

open NUnit.Framework
open System.Reflection

let ofList xs =
  List.fold (fun s x -> SearchTree.insert x s) SearchTree.empty xs

[<TestFixture>]
type SearchTreeTests () =

  [<Test>]
  member this.``toList empty is []`` () =
    Assert.That (SearchTree.toList (ofList ([]: int list)), Is.Empty)

  [<Test>]
  member this.``insert keeps the in-order list sorted`` () =
    let t = ofList [3; 1; 4; 1; 5]
    Assert.That (SearchTree.toList t, Is.EqualTo<int list> [1; 3; 4; 5])

  [<Test>]
  member this.``contains finds an inserted value`` () =
    let t = SearchTree.insert 7 SearchTree.empty
    Assert.That (SearchTree.contains 7 t, Is.True)

// A minimal test runner: find the fixtures and their tests by their
// attributes, call each test, report whether it raised an exception.
let runTests (asm: Assembly) =
  for fixture in asm.GetTypes () do
    if fixture.IsDefined typeof<TestFixtureAttribute> then
      let instance = System.Activator.CreateInstance fixture
      for test in fixture.GetMethods () do
        if test.IsDefined typeof<TestAttribute> then
          try
            test.Invoke (instance, [||]) |> ignore
            printfn "PASSED  %s" test.Name
          with e ->
            printfn "FAILED  %s\n%s" test.Name e.InnerException.Message

runTests typeof<SearchTreeTests>.Assembly

The same tests in a project

> dotnet new nunit -lang F# -o SearchTree.Tests
> cd SearchTree.Tests
> del UnitTest1.fs

Copy SearchTree.fsi and SearchTree.fs into the directory, save the fixture (without the runner) as Tests.fs with module Tests as its first line, and list the files in SearchTree.Tests.fsproj:

<ItemGroup>
  <Compile Include="SearchTree.fsi" />
  <Compile Include="SearchTree.fs" />
  <Compile Include="Tests.fs" />
  <Compile Include="Program.fs" />
</ItemGroup>

Program.fs is generated by the template and stays. Then:

> dotnet test
Passed!  - Failed:     0, Passed:     3, Skipped:     0, Total:     3, Duration: 19 ms - SearchTree.Tests.dll (net10.0)

Hansen's vectors

Hansen & Rischel's chapter 7 example: a module of geometric vectors behind a signature, with the operators defined as members of the type.

module Vector

[<Sealed>]
type Vector =
  static member ( ~- ) : Vector -> Vector
  static member ( + ) : Vector * Vector -> Vector
  static member ( - ) : Vector * Vector -> Vector
  static member ( * ) : float * Vector -> Vector
  static member ( * ) : Vector * Vector -> float

val make : float * float -> Vector
val coord : Vector -> float * float
val norm : Vector -> float

[lang=text]
module Vector

type Vector =
  | V of float * float
  static member ( ~- ) (V (x, y)) = V (-x, -y)
  static member ( + ) (V (x1, y1), V (x2, y2)) = V (x1 + x2, y1 + y2)
  static member ( - ) (V (x1, y1), V (x2, y2)) = V (x1 - x2, y1 - y2)
  static member ( * ) (a, V (x, y)) = V (a * x, a * y)
  static member ( * ) (V (x1, y1), V (x2, y2)) = x1 * x2 + y1 * y2
  override v.ToString () = match v with V (x, y) -> $"({x}, {y})"

let make (x, y) = V (x, y)
let coord (V (x, y)) = (x, y)
let norm (V (x, y)) = sqrt (x * x + y * y)

[lang=text]
> #load "Vector.fsi" "Vector.fs";;
> let a = Vector.make (1.0, -2.0);;
val a: Vector.Vector = (1, -2)
> let b = Vector.make (3.0, 4.0);;
val b: Vector.Vector = (3, 4)
> Vector.coord (2.0 * a - b);;
val it: float * float = (-1.0, -8.0)
> a * b, Vector.norm b;;
val it: float * float = (-5.0, 5.0)

The signature hides V, so a client makes vectors with make only, and the operators work on vectors without open Vector because they are members of the type. Hansen compiled the pair into a library with fsc -a and referenced the .dll; today a compiled library arrives as a package, and a pair of files is loaded with #load.

Exercises

Specifications only; no solutions here. Each of exercises 1–3 states examples; a hidden reference checks them when these notes are built.

Exercise 1: a stack with a hidden representation

Define a module Stack with a type 'a Stack whose representation a client cannot see, and

empty : 'a Stack
push : 'a -> 'a Stack -> 'a Stack
pop : 'a Stack -> ('a * 'a Stack) option
isEmpty : 'a Stack -> bool

Write example checks, then check the properties pop (push x s) = Some (x, s) and isEmpty (push x s) = false over at least five hand-written stacks with forAll.

Examples:

• pop empty is None.
• pop (push 1 empty) |> Option.map fst is Some 1.
• isEmpty empty is true, isEmpty (push 1 empty) is false.

Question: can a test of your module state the second property without toList-style access to the representation? Which property needs equality on stacks?

Exercise 2: find the bug

The function below is wrong.

let rec isSorted xs =
  match xs with
  | x :: y :: rest -> x <= y && isSorted rest
  | _ -> true

Write four example checks that pass. Then state the property that relates isSorted to List.sort, check it with forAll over hand-written inputs, and report the smallest input that fails.

Examples:

• isSorted [] and isSorted [1; 2; 3] are true.
• isSorted [3; 2; 1] is false.
• The smallest failing input has three elements.

Question: which inputs did your four passing checks never reach?

Exercise 3: a queue on two lists

Define type 'a Queue with a hidden representation of two lists (the front, and the back reversed — Lecture 8's accumulators), and

empty : 'a Queue
enqueue : 'a -> 'a Queue -> 'a Queue
dequeue : 'a Queue -> ('a * 'a Queue) option
toList : 'a Queue -> 'a list

A list is the model: check the equations toList (enqueue x q) = toList q @ [x] and dequeue q = (match toList q with [] -> None | y :: ys -> Some (y, …)), where the second component's toList is ys, over hand-written queues.

Examples:

• toList (enqueue 3 (enqueue 2 (enqueue 1 empty))) is [1; 2; 3].
• dequeue of that queue gives 1 and a queue whose toList is [2; 3].
• dequeue empty is None.

Question: when does dequeue reverse the back list, and how often does that happen over a long sequence of operations?

Exercise 4: your own tests

Take one function from a homework you have already submitted. Turn each clause of its task text into a named test in a fixture, in a script that #loads your homework file and #rs NUnit as Tests.fsx does, and run the fixture with runTests. Which clause had no test until now? (No stated values here: the function is yours.)