Code validation: from specifications to tests

Modules, NuGet, unit tests and the map of testing techniques

ITT8060 Advanced Programming · Autumn 2026

Tallinn University of Technology

How can code quality be assured based on specifications?

Full prose version with runnable examples: notes.html

ITT8060

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, "a type is a promise" (Lecture 5), factA n acc = acc * fact n (Lecture 8).

Lecture 8 derived code from a specification. Today the code is given, and we check it against the specification.

Plan: a specification says what · the module boundary · unit tests (NuGet, fixtures, runners) · properties and models · the map.

ITT8060

1 · A specification says what

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

ITT8060

Three forms you have already used

A type: val insert: x: 'a -> t: 'a BinTree -> 'a BinTree when 'a: comparison (Lecture 6). A promise for every input; the compiler checks it.

An example: "contains 13 t should return true" (every homework's "e.g."). A test checks it.

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

Validation compares the code with the specification.

ITT8060

Which form is it?

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

A type — the compiler checks it, for every input, before the program runs.
An example — a unit test (concept 3).
An equation — a property test over many inputs (concept 4), or a derivation (Lecture 8).
An invariant — a property test over many trees, or enforced at a module boundary (concept 2).
A model — compare with the simpler implementation on the same inputs (concept 4).

ITT8060

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

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

check "fact 0" 1 (fact 0)
check "fact 3" 6 (fact 3)
check "fact 5" 120 (fact 5)

A check on a point

All three checks pass. Is fact correct?

What is fact 7?

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

A check on a point says nothing about the other points.

ITT8060

2 · The module boundary

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

ITT8060

From Lecture 6

'a BinTree with Empty and Node; insert, contains, inOrder. The search-tree invariant: in every Node (l, x, r), all of l is less than x and all of r is greater.

t (left) satisfies it. bad = Node (leaf 5, 3, Empty) (right) does not, and the type does not care.

What is inOrder (insert 4 bad)?

[5; 3; 4] — not sorted. "Garbage in, garbage out."

ITT8060

The tree insert 4 bad.

Garbage in, garbage out

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

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

isSearchTree t is true; isSearchTree bad is false.

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

ITT8060

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

let greeting1 = Greeting.greet "Mari"

open Greeting
let greeting2 = greet "Jaan"

Modules

Every script and every file is a module (Lecture 2: "the toplevel of the module"). A module can also be declared inside a script.

Members are used with the module's name in front, or after open.

prefix is private: visible inside Greeting, invisible outside.

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

ITT8060

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

let boiling = Temperature.toFahrenheit 100.0

Qualified access

Lecture 5 wrote Set.add, Map.find, List.map — never open Set. The attribute keeps a module's short names out of your script.

> open Temperature;;
error FS0892: This declaration opens the
module 'FSI_0001.Temperature', which is
marked as 'RequireQualifiedAccess'. ...

Our search tree module is marked the same way.

ITT8060

[<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

A search tree module

A search tree is a binary tree 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. The insert on the right is Lecture 6's.

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

SearchTree.toList st is [4; 7; 9].

ITT8060

What can a client do?

Build 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: every 'a SearchTree satisfies it. The invariant has become a promise of the type.

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 the representation, and survives a change of representation.

ITT8060

Files are modules

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

A file sees only the files loaded before it:

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

No cycles; a project lists its files in the same order.

A namespace names a group of modules and types across files (namespace Itt8060.Lecture9); a script cannot declare one.

ITT8060

The signature file

SearchTree.fsi: the interface written down — the val lines, 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

#load "SearchTree.fsi" "SearchTree.fs" loads the signature first; the compiler checks the implementation against it.

ITT8060

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'

For a client, the constructor does not even exist:

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

A specification a client can bypass is a comment. Behind a module boundary it is a guarantee, and tests of the module test the guarantee.

ITT8060

3 · Unit tests

A unit test makes one example of the specification executable.

ITT8060

check "contains 13 t" true (contains 13 t)
check "contains 8 t" false (contains 8 t)
check "inOrder" [2; 7; 9; 13; 21; 25] (inOrder t)

A plain check

We have one already: check from concept 1. These notes' exercises are checked the same way when the notes are built: a hidden reference is applied to the stated examples, and a mismatch stops the build.

Missing for a suite: a name for each test, a report that lists them, one command to run them all.

A library provides that. First, how to get a library.

ITT8060

NuGet: where libraries come from

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

#r "nuget: NUnit, 4.3.2"

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

> #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: no network.

Then open NUnit.Framework, and the API from the package's documentation: Assert.That (actual, Is.EqualTo expected), Is.True, Is.Empty.

ITT8060

NuGet: caveats

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

> #r "nuget: NUnit";;
[Loading ...\nuget\Projects\38696--c955...382b\Project.fsproj.fsx]
> typeof<NUnit.Framework.TestAttribute>.Assembly.GetName().Version;;
val it: System.Version = 5.0.0.0 {...}

The newest release on the day (2026-10-28). Next month: perhaps another, with another behaviour. A script others will run pins its version.

This lecture pins 4.3.2, the version the .NET 10 SDK's test template uses.

A package brings its dependencies along (fsharp.core 10.1.302 arrived with NUnit). A project lists the same packages as package references in its project file — in a moment.

ITT8060

A fixture

A test script loads NUnit and the module, then declares a fixture: a type whose members are the tests — the shape of the course's own tests. (ofList folds insert over a list.)

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

[<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])

ITT8060

Arrange, act, assert

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

The name is a sentence of the specification, in double backticks so that it may contain spaces. The report lists the names: the report reads as the specification.

[<Test>] marks a member as a test, [<TestFixture>] a type as a group of tests. Is.EqualTo<int list>: NUnit has three EqualTo overloads and F# cannot choose one for a list; the type argument says which.

ITT8060

Running a test is calling it

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

A loaded script is a module named after the file.

A test is a function: () when the assertion holds, an exception when it does not. That is all there is to it.

ITT8060

How a runner works

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

Discovery by attributes, every [<TestFixture>] type and every [<Test>] method; invoke each test; an exception is a failure. runTests typeof<SearchTreeTests>.Assembly at the end of the script.

ITT8060

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

NUnit's message: the test, the expected value, the actual one.

ITT8060

What the real runner adds

Ours lacks:

Isolation — NUnit records failures in a context our runner never resets; call the failing test by hand after the run and the message lists the failure twice.
Time limits — a test that loops forever hangs our runner.
Parallel runs and a report in a standard format.

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

ITT8060

The same tests in a project

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

The module, its signature and the fixture (under module Tests, no runner) as compile items, in order; the packages as references:

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

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

dotnet test restores them (the framework, the adapter that finds the tests, the test host), builds and runs:

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

ITT8060

How your homework is graded

The course's automated tests work the same way, in scripts:

Your script is copied under a fixed name and loaded as a module, as SearchTree.fs was.
One fixture per task holds the tests of that task's clauses, named as the clauses are: the names in your report are the members' names.
A task's grade is the share of its tests that pass.
Each test has a time limit: a function that loops forever fails instead of hanging the run.
Some tests are property-based: a tool chooses their inputs. Next week.

ITT8060

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.

ITT8060

4 · Properties and models

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

ITT8060

The "oracle" problem

Every check needs an expected result — an "oracle" that knows the answer.

An example: you compute it by hand (fact 5 is 120). Cheap; 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). Checkable 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.

ITT8060

Properties are equations

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 for these pairs?

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

false; the first failing pair is ([1], [2]). Reversing swaps the halves: rev (xs @ ys) = rev ys @ rev xs holds on all four.

And fact n = n * fact (n - 1) over 1 .. 10? false, at 7. A property is a specification; checking it over inputs is a test of the specification itself.

ITT8060

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 x in 0, 4, 11?

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: no hand-computed answers.

ITT8060

Next week, and the week after that

Both checks 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, a failing input is "shrunk" to a smallest one that still fails. In F#: 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.

ITT8060

5 · The map

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

ITT8060

The map of testing techniques

Technique	Specification	Who chooses the inputs	Finds	Cannot find
Type checking	types	the compiler, for all inputs	shape errors, before the run	wrong values
Unit tests	examples	you	the cases you thought of	everything else
Property-based tests	equations, invariants	a generator	the cases you did not think of	what the generator never produces
Model-based tests	a model	a tool, exploring sequences	wrong sequences of operations	what the model also gets wrong
Runtime checks	invariants, preconditions	the real users	violations in production, late	anything before it runs
Proof	any statement	nobody: all inputs at once	every error, at the cost of a proof	mistakes in the specification

ITT8060

Where does it go?

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

Type checking — a type; the compiler chose every input.
A unit test — an example; you chose the input.
A property-based test — an equation, over inputs a tool can choose.
A model-based test — a model, over sequences of operations.
A runtime check — an invariant, on the inputs the real users supply.

ITT8060

The answer

How can code quality be assured based on specifications?

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

ITT8060

Summary

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

ITT8060

Other tools you will meet

FsUnit: assertions that read as sentences on top of NUnit, actual |> should equal expected. Its release must match the NUnit version (FsUnit 8 needs NUnit 5: not the 4.3.2 pinned here).
Expecto: F#-native; tests are values, testCase "name" <| fun () -> ..., in lists, run from a script or a console program. No attributes.
xUnit: the other common .NET framework; [<Fact>] for [<Test>], dotnet new xunit.
FsCheck: property-based testing. Next week.

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

ITT8060

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 on modules, namespaces, signature files and package references in F# Interactive; the NUnit documentation.

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

The complete module, signature and test script, the project, and the exercises: the Worked examples and Exercises sections of notes.html.

ITT8060