DEV Community: Kuniwak

Debugging BLE macros on Nature Remo was such an ordeal that I built a Swift development environment

Kuniwak — Mon, 28 Apr 2025 02:40:36 +0000

TL;DR

I have prepared an environment for developing a subset of Android nRF Connect BLE macros on macOS, iOS, and other Apple platforms.

Kuniwak / swift-ble-macro

BLE (Bluetooth Low Energy) Macros for Swift

swift-ble-macro

This is a simple Swift library that allows you to easily create nRF Connect BLE macros ¹ for your iOS/iPadOS/macOS/watchOS/visionOS/tvOS app It is a wrapper around Core Bluetooth that allows you to create macros for BLE devices. It is designed to easily develop Nature Remo compatible BLE macros².

Installation

Add the following to your Package.swift file:

.package(url: "https://github.com/Kuniwak/swift-ble-macro.git", from: "<version>")

Products

Product	Description
`BLEMacroEasy`	Defines the easy interface to execute BLE macros.
`BLEMacro`	Defines the BLE macro XML parser.
`BLEMacroCompiler`	Defines the BLE macro compiler that compile BLE macro XML to BLE macro IR.
`BLECommand`	Defines the BLE macro IR.
`BLEInterpreter`	Defines the BLE macro interpreter that interprets BLE macro IR.
`BLEInternal`	Defines the utilities for BLE macros.
`BLEModel`	Defines the convenient state machines for BLE.

Supported Macros

Currently, only the following BLE macro XML elements…

View on GitHub

import Foundation
import BLEMacroEasy

// You can find your iPhone’s UUID by running the commands below in Terminal:
// $ git clone https://github.com/Kuniwak/swift-ble-macro
// $ cd swift-ble-macro
// $ swift run ble discover
let myIPhoneUUID = UUID(uuidString: "********-****-****-****-************")!
let myMacro = try String(contentsOf: URL(string: "https://ble-macro.kuniwak.com/iphone/battery-level.xml")!)

try await run(macroXMLString: myMacro, on: myIPhoneUUID) { data in
    // This handler is called every time a value is read from the peripheral.
    let batteryLevel = Int(data[0])
    print("\(batteryLevel)%")
}

Besides the ability to run BLE macros on macOS/iOS/…, the project also provides a CLI that helps you develop those macros.
For the macro-execution API, see the README.
The CLI supports device scanning, macro validation, macro execution, and an interactive REPL:

$ # Scan BLE devices
$ ble discover
00000000-0000-0000-0000-000000000000    Example Device 1    -78
11111111-1111-1111-1111-111111111111    Example Device 2    -47
22222222-2222-2222-2222-222222222222    Example Device 3    -54
...

$ # Abort scanning with Ctrl+C

$ # Run a BLE macro
$ ble run path/to/your/ble-macro.xml --uuid 00000000-0000-0000-0000-000000000000

$ # Run a BLE macro interactively
$ ble repl --uuid 00000000-0000-0000-0000-000000000000
connecting...
connected

(ble) ?
write-command, w, wc            Write to a characteristic without a response
write-descriptor, wd            Write to a descriptor
write-request, req              Write to a characteristic with a response
read, r                         Read from a characteristic
discovery-service, ds           Discover services
discovery-characteristics, dc   Discover characteristics
discovery-descriptor, dd        Discover descriptors
q, quit                         Quit the REPL

(ble) dc
180A 2A29 read
180A 2A24 read
D0611E78-BBB4-4591-A5F8-487910AE4366 8667556C-9A37-4C91-84ED-54EE27D90049 write/write/notify/extendedProperties
9FA480E0-4967-4542-9390-D343DC5D04AE AF0BADB1-5B99-43CD-917A-A77BC549E3CC write/write/notify/extendedProperties
180F 2A19 read/notify
1805 2A2B read/notify
1805 2A0F readk

(ble) r 180F 2A19
58

The BLE macros I have written are published at Kuniwak/ble-macro.

Background

Nature Remo recently gained a Bluetooth Low Energy (BLE) macro feature (official announcement).
If you own a compatible model (Nature Remo 3 or Nature Remo mini 2 family), you can control BLE devices directly from your Remo.
I therefore started writing BLE macros so that our three full-colour Philips Hue bulbs could be driven from Remo (I have always had a faint admiration for scenes like this video, hence the extravagant colours).

The macros supported by Remo are a subset of those used by Android nRF Connect.
Macros are written in XML. For example, to turn a Hue bulb on in daylight-white you can write:

<macro name="hue-daylight-white" icon="BRIGHTNESS_HIGH">
    <assert-service description="Hue" uuid="932c32bd-0000-47a2-835a-a8d455b859dd">
        <assert-characteristic description="Combined" uuid="932c32bd-0007-47a2-835a-a8d455b859dd">
            <property name="WRITE" requirement="MANDATORY"/>
        </assert-characteristic>
    </assert-service>
    <write description="Set to Daylight White"
           characteristic-uuid="932c32bd-0007-47a2-835a-a8d455b859dd"
           service-uuid="932c32bd-0000-47a2-835a-a8d455b859dd"
           value="0101010201fe0302fa0005020100"
           type="WRITE_REQUEST" />
</macro>

With BLE macros you instruct read/write operations against services and characteristics.
For well-known devices you can often find the details thanks to specifications reverse-engineered by third parties, but bringing a hand-written macro to a “working on Remo” state still requires a fair bit of trial and error. And that trial and error was utterly painful.

According to the documentation, Android users can rely on the nRF Connect for Mobile app, which supports everything from recording to running BLE macros, making development easy.
Unfortunately I had no Android device at hand.
There is an iOS version by the same developer, but it does not include the macro feature.
In the beginning I was stuck in a loop of feeding a macro to Remo, hitting a barely-described error, tweaking the XML by guesswork, and trying again…

Because this cycle was so fruitless, I decided to build an environment with functionality similar to Android’s nRF Connect for Mobile.
That is how Kuniwak/swift-ble-macro was born.
Although it offers only a subset of features compared with nRF Connect, it is more than enough to develop BLE macros that run on Remo. Feel free to give it a try!

When developing macros it is also important to capture what traffic an existing app is exchanging with the BLE device.

BLE-macro Growing Pains

During my adventures with Hue and Switchbot I ran into all sorts of issues; let me document them here for posterity.

Hue returns an insufficient encryption error

Hue bulbs cannot be operated unless they are paired.
Attempting to read/write from a non-paired central results in an insufficient encryption error.
Only the first device that performs pairing gets registered (there is a workaround, explained below).
For example, if you connect using the official Hue app first, any subsequent device (e.g. Remo or Google Nest mini) will be rejected.

You can work around this by opening Hue app › Settings › Voice assistant › Google Home › Make discoverable.
This puts the bulb into a discoverable state for a very short time (about a minute).
Programmatically, the same effect can be achieved by writing 0x01 to characteristic 97fe6561-2004-4f62-86e9-b71ee2da3d22 of service 0000fe0f-0000-1000-8000-00805f9b34fb (see the make-discoverable BLE macro).

No clear factory-reset procedure after a failed Hue pairing

If your Hue bulb gets paired to, say, a Google Nest mini before you manage to pair it with the official app or a Mac, the insufficient encryption problem prevents any further operation, including factory reset, because that too is done over BLE.

Some guides propose toggling the power repeatedly to reset the bulb — for example this discussion.
However, this did not work for my bulb (model LCA009, firmware v1.116.3).
What did work was cutting the power at the wall switch, then turning it back on; for a brief moment and at very close range the official Hue app could see the bulb again, from which I was able to perform a factory reset.

Switchbot does not respond

Switchbot devices can also be controlled via BLE, but they are finicky.
For firmware v6.6 you can operate them with the macro shared in the developer community on Discord, but v6.3 ignores the same commands.
After some trial and error I discovered that, on v6.3, subscribing to notifications on characteristic cba20003-224d-11e6-9fb8-0002a5d5c51b before writing 0x01 to cba20002-224d-11e6-9fb8-0002a5d5c51b makes the arm move.
Here is a macro that works on v6.3:

<macro name="switchbot-push" icon="PLAY">
    <assert-service description="Switchbot" uuid="cba20d00-224d-11e6-9fb8-0002a5d5c51b">
        <assert-characteristic description="Push" uuid="cba20002-224d-11e6-9fb8-0002a5d5c51b">
            <property name="WRITE" requirement="MANDATORY"/>
        </assert-characteristic>
        <assert-characteristic description="Configuration" uuid="cba20003-224d-11e6-9fb8-0002a5d5c51b">
            <property name="NOTIFY" requirement="MANDATORY"/>
            <assert-cccd />
        </assert-characteristic>
    </assert-service>

    <write-descriptor description="Enable notifications"
                      characteristic-uuid="cba20003-224d-11e6-9fb8-0002a5d5c51b"
                      service-uuid="cba20d00-224d-11e6-9fb8-0002a5d5c51b"
                      uuid="00002902-0000-1000-8000-00805f9b34fb"
                      value="0100" />

    <write description="Write 0x570100"
           characteristic-uuid="cba20002-224d-11e6-9fb8-0002a5d5c51b"
           service-uuid="cba20d00-224d-11e6-9fb8-0002a5d5c51b"
           value="570100"
           type="WRITE_REQUEST" />

    <wait-for-notification description="Wait for notification"
                           characteristic-uuid="cba20003-224d-11e6-9fb8-0002a5d5c51b"
                           service-uuid="cba20d00-224d-11e6-9fb8-0002a5d5c51b"
                           timeout="5000" />
</macro>

Products and References I Found Helpful

jnross / Bluetility

A Bluetooth Low Energy browser, an open-source alternative to LightBlue for OS X

Bluetility

Bluetility is a general-purpose Bluetooth Low-Energy utility for Mac OS X. It scans for advertising peripherals, provides a interface to browse a connected peripheral's services and characteristics, and allows characteristic values to be read, written, and subscribed

Installation

Manual

Download the latest release: https://github.com/jnross/Bluetility/releases/latest/download/Bluetility.app.zip
Extract the downloaded archive.
Move Bluetility.app into your /Applications folder. Or don't!
Open Bluetility.app.

Using Homebrew

brew install --cask bluetility

Features

Scan for nearby advertising peripherals
Sort peripherals by received signal strength
View advertising data via tooltip on Devices list
Browse services and characteristics of connected peripheral
Subscribe to characteristic notifications
Read/Write characteristic values
View log of characteristic read/writes, logs may be saved as CSV

Motivation

Bluetility is inspired by LightBlue, a free bluetooth utility published by Punch Through Design. Bluetility was created to resolve issues in this tool, and add missing features:

Support copy/paste via Cmd+C and Cmd+V
Sort peripherals by received…

View on GitHub

OpenWonderLabs / SwitchBotAPI-BLE

SwitchBot BLE open API

SwitchBotAPI-BLE

Device Types

Product	Device Type
Bot	H (0x48)
Meter	T (0x54)
Humidifier	e (0x65)
Curtain	c (0x63)
Curtain 3	{(0x7B)
Motion Sensor	s (0x73)
Contact Sensor	d (0x64)
Color Bulb	u (0x75)
LED Strip Light	r (0x72)
Smart Lock	o (0x6F)
Plug Mini	g (0x67)
Meter Plus	i (0x69)

The device type is in the service data of SCAN_RSP.

Service data
Byte: 0	Enc type	Bit[7] NC
Byte: 0	Dev Type	Bit [6:0] – Device Type

UUID Update Notes

From Bot V6.4, Curtain V4.6, Meter V2.7,

Company ID ( ADV_IND - Manufacture Data ) modified from 0x0059…

View on GitHub

Software Testing: Theory and Practice (Part 8) - One Step Beyond

Kuniwak — Mon, 28 Apr 2025 02:15:14 +0000

Key Takeaways

Every form of software testing we have examined so far samples the input space. Any inputs that fall outside the sample are never exercised, creating risk.
In some projects this risk is unacceptable. In such cases, formal methods—which allow exhaustive verification—become an attractive option.

Challenges of Traditional Software Testing

To conclude this series, we will spend two installments looking at technologies that go one step beyond traditional software testing.

In Part 1 “Fundamental Concepts of Software Testing” and Part 2 “Software Testing and Logical Expressions,” we explained that software testing of functional systems means confirming that, for every input satisfying the pre-conditions, the output
satisfies the post-conditions. Exhaustively exercising every possible input is, however, prohibitively expensive.

Consequently, as discussed in Part 5 “How to Select Test Cases,” we finish testing after examining only a subset of inputs, then extrapolate the overall risk from that subset’s results. Inputs that were not selected remain untested, and defects may
well lurk there. Most of us have triggered a software failure at some point in daily life; almost invariably that failure was caused by an input never chosen as a test sample.

Failures caused by out-of-sample inputs are not rare. In other words, traditional sampling-based testing deliberately trades lower cost for a non-trivial amount of risk—and we should stay aware of that fact.

Sometimes a project simply cannot take that risk—for example, aerospace, transportation, or medical systems demanding high reliability. Even where the reliability bar is lower, Part 3 “The Significance and Strategy of Shift-Left Testing” showed that the earlier we detect defects, the cheaper they are to remove. From a cost
perspective alone, a project may therefore prefer heavier early-stage testing.

When you want exhaustive verification rather than sampling, formal methods are invaluable. Across this two-part finale we will start with a single sample in a traditional test, gradually increase the number of test cases, and eventually arrive at formal methods that cover all inputs. Along the way we will observe
what we gain—and what we lose.

What Happens as We Add Test Cases ?

When There Is Only One Test Case

Let’s begin with just one test case, i.e. one input/output pair.
In traditional Example-Based Testing (EBT) we supply a concrete input and the expected output, then compare the actual output:

Suppose we have our own natural-number type—ZERO, ONE, TWO, …—and an
add function. To verify that 1 + 1 = 2, an EBT looks like Listing 1.

Listing 1. First test case for the natural-number addition

// Verify that our custom addition returns 2 for 1 + 1
describe('add', () => {
  context('when given 1 + 1', () => {
    it('returns 2', () => {
      // Provide concrete inputs
      const actual = add(ONE, ONE);
      // Provide the expected output
      const expected = TWO;
      // Compare actual and expected; fail if they differ, succeed if they match
      assert.deepStrictEqual(actual, expected);
    });
  });
});

Of course, checking only $1 + 1$ is hardly reassuring, so we add more cases.

When There Are Two Test Cases

To verify 1 + 0 = 1 as well, we might simply add another almost identical block, as in Listing 2.

Listing 2. Two separate test cases

describe('add', () => {
  // Original test case
  context('when given 1 and 1', () => {
    it('returns 2', () => {
      const actual = add(ONE, ONE);

      const expected = TWO;
      assert.deepStrictEqual(actual, expected);
    });
  });

  // Additional input goes in its own test case
  context('when given 1 and 0', () => {
    it('returns 1', () => {
      const actual = add(ONE, ZERO);

      const expected = ONE;
      assert.deepStrictEqual(actual, expected);
    });
  });
});

But this approach needs roughly eight lines for every added case—verbose and error-prone. Instead, we can share the common scaffolding by supplying the input/expected pairs in table form, as in Listing 3. Such tests are called Parameterized Tests or Table-Driven Tests.

Listing 3. Converted to a parameterized test

describe('add', () => {
  // Table of input and expected output
  // lhs = left-hand side, rhs = right-hand side
  [
    { lhs: ONE, rhs: ONE,  expected: TWO },
    { lhs: ONE, rhs: ZERO, expected: ONE },
  ]
  .forEach(({ lhs, rhs, expected }) => {
    context(`${lhs} + ${rhs}`, () => {
      it(`returns ${expected}`, () => {
        const actual = add(lhs, rhs);

        assert.deepStrictEqual(actual, expected);
      });
    });
  });
});

Now each extra test case costs just one new line.

Column: Eager Tests

You often see code that tries multiple inputs within a single test case—the anti-pattern known as an Eager Test. It has two problems:

If the first assertion fails, later assertions never run, so diagnostic information is limited.
Bundling multiple inputs under one case blurs the test’s intent, because the case name can no longer describe exactly what is being verified.

The recommended style is one input → one test case, as shown here.

If We Keep Increasing the Number of Test Cases

How many cases are enough to trust our addition? Certainly more than two. To identify good cases we would like to use the On–Off Point method, introduced in Part 5 “How to Select Test Cases.”
However, that method assumes (1) the implementation performs a top-level branch with no loops/recursion afterwards—an assumption our add does not meet. In such situations Property-Based Testing (PBT) is more suitable.

Recap: PBT automatically generates large numbers of inputs. Because the inputs are generated, we can’t specify concrete expected outputs. Instead we supply a relationship that must hold between each input and its output.

Listing 4. Skeleton of a property-based test

describe('add', () => {
  context('given x and 0', () => {
    it('returns ???', () => {
      const x = valuesGen(); // generator picks some natural number
      const actual = add(x, 0);

      const expected = '???'; // concrete expectation unavailable
      assert.deepStrictEqual(actual, expected);
    });
  });
});

Thus, we replace explicit outputs with properties.

Part 4 suggested using the post-condition as that property. Table 1 restates the specification of add.

Table 1. Specification of add

Left operand	Right operand	Output
0	0	0
0	1	1
0	2	2
…	…	…
1	0	1
1	1	2
1	2	3
…	…	…

Unfortunately, expressing this relation without using “add two natural numbers” is difficult—yet that is exactly what we are implementing. So we fall back to a simpler property: the commutative law.

Listing 5. Verifying that add(x, 0) equals x

describe('add', () => {
  context('given x and 0', () => {
    it('returns x', () => {
      const [x, y] = valuesGen(); // generator picks x and y
      const actual   = add(x, y);
      const expected = add(y, x); // commutativity
      assert.deepStrictEqual(actual, expected);
    });
    // In practice valuesGen runs many times with different inputs.
  });
});

This alone is not sufficient—an implementation that mistakenly performs multiplication would still pass—so we add more relations (Listing 6).

Listing 6. Additional properties for addition

describe('add', () => {
  context('given x and 0', () => {
    it('returns x', () => { /* … */ });
  });

  context('given x and y + 1', () => {
    it('returns (x + y) + 1', () => { /* … */ });
  });

  context('given x and y', () => {
    it('returns the same as y + x (commutativity)', () => { /* … */ });
  });

  context('given x and y, then adding z to the result', () => {
    it('matches adding x to (y + z) (associativity)', () => { /* … */ });
  });

  // valuesGen runs many variations.
});

Automatic generation lets us exercise far more inputs than hand-written cases ever could. What we lose is concreteness: we must discover and encode abstract input/output relationships—a skill that takes practice.

Even here the space is not fully covered; the generated values, though numerous, are still a tiny subset of all natural numbers. One extension is to shrink the input domain until exhaustive testing becomes feasible (e.g. by imposing a maximum value). But sometimes we cannot lower that maximum. That is where formal methods shine.

What Are Formal Methods ?

Formal methods are mathematically based techniques for specifying, developing, and verifying software and hardware. The field is vast and rapidly evolving; we cannot cover everything here. Instead, we will demonstrate a proof assistant, one category of formal-methods tools.

Exhaustive Testing with a Proof Assistant

We will use the proof assistant Isabelle¹ to exhaustively verify the wide input space.

A proof assistant lets you define programs (like an ordinary language) and prove mathematical properties about them. Crucially, logical quantifiers such as “for all x” allow statements about every possible input—transcending the limits of traditional and property-based tests.

Consider the Pythagorean theorem: for the legs $a$ , $b$ and hypotenuse $c$ of a right triangle, $a^2 + b^2 = c^2$ always holds. Checking a handful of triangles does not prove the universal claim, just as testing can never prove the absence of all defects. Mathematical proof does.

Isabelle

We will translate the earlier JavaScript add into Isabelle².

Listing 1. JavaScript version of add

// Inputs are Zero or Succ.
// Zero represents 0; Succ(n) is n + 1.
// new Succ(new Zero()) is 1,
// new Succ(new Succ(new Zero())) is 2, and so on.
class Zero {}
class Succ {
  constructor(nat) { this.v = nat; }
}

function add(a, b) {
  // Base case: if b is 0 then a + 0 = a
  if (b instanceof Zero) {
    return a;
  }
  // Recursive case: a + b = Succ(a + (b − 1))
  return new Succ(add(a, b.v));
}

Listing 2. Isabelle version of add

theory Scratch
  imports Main
begin

datatype myNat = Zero | Succ myNat

primrec add :: "myNat ⇒ myNat ⇒ myNat"
  where "add a Zero     = a"
      | "add a (Succ b) = Succ (add a b)"

(* ... more to come ... *)

end

Proving Program Behaviour

First, we replicate the property from PBT: $x + 0 = x$ .

Listing 3. Proof that $x + 0 = x$

lemma add_Zero_eq:
  shows "add x Zero = x"
  by (induct x; auto)

(* cursor here *)

Isabelle reports (excerpt):

theorem add_Zero_eq:
add ?x Zero = ?x

To see a failed proof, change 0 to 1 (Listing 5).

Listing 5. Attempting (and failing) to prove $x + 1 = x$

lemma add_One_eq:
  shows "add x (Succ Zero) = x"
  by (induct x; auto)

(* cursor here *)

Output:

theorem add_One_eq:
add ?x (Succ Zero) = ?x
Failed to finish proof⌂:
goal (1 subgoal):
    1.  False

Was the claim false, or merely too hard for automation? Isabelle’s try
command helps distinguish the two, by invoking Nitpick, Quickcheck, and
Sledgehammer.

Listing 7. Using try

lemma add_One_eq:
  shows "add x (Succ Zero) = x"
  try

Output:

Trying “solve_direct”, “quickcheck”, “try0”, “sledgehammer”, and “nitpick”…
Nitpick found a counterexample:
Free variable:
x = Succ (Succ Zero)

Nitpick found x = 2, confirming the statement is false.

Similarly we can prove the remaining properties (Listing 9).

Listing 9. Proving the remaining properties

lemma add_Succ_eq:
  shows "add (Succ x) y = Succ (add x y)"
  by (induct y; auto)

lemma
  shows "add x y = add y x"
  by (induct y; auto simp add: add_Zero_eq add_Succ_eq)

lemma [simp]:
  shows "add (add x y) z = add x (add y z)"
  by (induct z; auto)

And because Isabelle provides mathematical naturals, we can easily verify the post-condition as well (Listing 10).

Listing 10. Proving the post-condition

fun denoteMyNat :: "myNat ⇒ nat"
  where "denoteMyNat Zero     = 0"
      | "denoteMyNat (Succ x) = 1 + denoteMyNat x"

lemma
  shows "denoteMyNat (add x y) = denoteMyNat x + denoteMyNat y"
proof (induct x)
  case Zero
  thus ?case by (induct y; auto)
next
  case (Succ x)
  thus ?case by (simp add: add_Succ_eq)
qed

A full Isabelle tutorial—e.g. Programming and Proving in Isabelle/HOL³—
is beyond our scope, but highly recommended.

Summary

Using natural-number addition as an example, we observed this progression:

Number of test cases	Technique
A handful	Traditional example-based test
Dozens	Parameterized test
Hundreds	Property-based test
All inputs	Formal methods

Moving from stage ① to ② is easy and loses nothing.
From ② to ③ we lose concrete inputs/outputs; from ③ to ④ we additionally need
mathematical-proof skills. The lower we go, the more abstract our description
must become to keep maintenance feasible.

Mastering formal methods takes training. Humans rarely write perfect logical
statements or proofs on the first try—just as we rarely write bug-free code.
Hence we must verify that our own formulas and proofs match our intent.
Understanding the messages produced by tools like Isabelle therefore requires
a solid grounding in logic, and process skills akin to Test-Driven Development
help enormously.

I hope this article sparks your interest in formal methods.

https://isabelle.in.tum.de/index.html ↩
A rigorous correspondence would require a formal semantics for JavaScript, which is beyond our scope here. ↩
https://isabelle.in.tum.de/dist/Isabelle2024/doc/prog-prove.pdf ↩

Software Testing: Theory and Practice (Part 7) - Fundamentals and Strategies for Integration & E2E Testing

Kuniwak — Sun, 27 Apr 2025 02:27:57 +0000

Key Takeaways

Integration tests can uncover integration bugs caused by specification mismatches between components that unit tests cannot detect. Their downsides are long execution times, flaky results, and high maintenance costs.
To keep maintenance costs low, minimize the number of integration-test cases and compose them from high-value test scenarios.
Combine them with “autopilot”–style tests that require no explicit scenarios.

Characteristics of Integration & E2E Testing

Integration testing targets a group of components combined together.
Unlike unit tests—where all dependencies are replaced with test doubles—integration tests run the real components.
Because some of those components may have long processing times, test runs tend to be slow.
If the components communicate over a network, disconnections or latency can also make results unstable.

E2E (end-to-end) testing exercises the entire system with all components integrated.
Since more components are involved, execution takes even longer, and E2E tests inherit the same flakiness issues.

Despite these drawbacks, integration and E2E tests remain indispensable because they can detect integration bugs earlier than system-level manual testing.
An integration bug is a defect arising from a mismatch between the specifications of two or more components.

Example: Component A outputs a string, while Component B expects an integer.
Each component individually satisfies its own specification, so their unit tests pass.
But when they are wired together in a dynamically-typed language, a run-time type error can occur.
Other examples include misunderstandings of a dependency’s API or unintended states/transitions when concurrently running components interact.

Integration—and especially E2E—targets almost invariably hold state.
As you combine more components, the state space explodes, so any practical test can explore only a tiny fraction of all possible states.

Here are two keys to successful integration/E2E testing:

Cover the tiny fraction you can test with high-value scenarios.
Use scenario-free tests to coarsely cover the vast remainder of the state space.

We start with choosing high-value scenarios.

Column: Formal Specification Descriptions

Because integration bugs stem from spec mismatches, they could be caught during specification writing—if specifications are written in a machine-checkable form.
Such techniques are known as formal specification descriptions.
A concise explanation is beyond this article’s scope.

Choosing High-Value Scenarios

In this article, a test scenario consists of

a sequence of events fed into the integrated system, and
an oracle that judges the final state.

An event is anything that triggers a change of internal state—method calls, network messages, UI actions, and so on.
Events also represent interaction: one event can simultaneously change several components (e.g., a request alters both client and server state).

In short, a scenario executes events in a prescribed order/timing and then inspects the resulting state.
If an exception or crash occurs during the sequence, the test fails.

Below is a sample E2E scenario for a login screen:

describe("Login screen", () => {
  context("When a valid user name and password are entered and the Login button is pressed", () => {
    it("navigates to the Welcome screen", async () => {
      // Event: open the login page
      await driver.get("https://example.com/login");

      // Event: type “kuniwak” into the user name field
      await driver.findElement(By.id("input.username")).sendKeys("kuniwak");

      // Event: type “p4$SW0rD” into the password field
      await driver.findElement(By.id("input.password")).sendKeys("p4$SW0rD");

      // Event: click the Login button
      await driver.findElement(By.id("button.login")).click();

      // Assert navigation to a page whose <title> is “Welcome”
      await driver.wait(until.titleIs("Welcome"), 1000);
    });
  });
});

The value of a scenario is how much its success reduces failure risk.
Higher-risk-reduction ⇒ higher value.

High-value scenarios fall into two patterns:

High-frequency: executed often in production (typical happy paths).
High severity on failure: even if rare, a defect would be catastrophic.

High-frequency examples
The login path of a service that every user must pass through is high-value because of sheer usage volume.
Analyzing user behavior—e.g., with Google Analytics—helps identify such paths.
Because user behavior evolves, repeat this analysis periodically.

High-severity examples
Payment failure flows rarely occur, but if they do—charging without delivering goods or vice versa—the impact is huge.
Thus payment scenarios are likewise high-value.

To identify high-severity cases, interview people who best understand how the system creates value—domain experts—and enumerate what could go wrong.
For an e-commerce site, two expert-provided scenarios might be:

User flow: discover the site → find an item → add to cart → fill in details → pay → receive purchase.
Service flow: procure popular items → store them → promote → ship according to user payments.

If the site fails at any step of either flow and no recovery is possible, the store ceases to function.
Both flows therefore deserve E2E protection.

Conversely, auxiliary features around high-value flows—e.g., wish-list management or viewing order history—might be left untested if their failure is tolerable or operationally recoverable.
But if a wish-list differentiates you from competitors, or customer-service costs are huge, these become high-value too.
The assessment is case-by-case; interview as many domain experts as possible for a broad view.

If experts are unavailable, risk-analysis techniques such as STAMP/STPA can help.

Selecting such scenarios lets you cut failure risk with few tests.
But scenario-based tests are costly to maintain, so limit them to high-value paths and complement the rest with scenario-free tests.

Combining Scenario-Free Tests

Scenario-free tests include model checking and property-based testing (PBT)—especially fuzzing.
We outlined them in Part 4 and detailed PBT in Part 5.

Model checking exhaustively explores a system’s state space to verify properties.
Property-based testing auto-generates inputs while humans supply properties relating inputs and outputs. When the only property is “no exception/crash,” the practice is called fuzzing.

Their advantage: even without concrete scenarios, they can roughly test vast areas that high-value scenarios never visit.
Example: a crawler that follows every link on a site and asserts no 5xx status or client-side error.
It checks that reachable pages at least don’t error out—though it can’t verify you landed on the intended page, so it is “coarser” than scenario-based E2E tests.

A common pain point is wasting time revisiting already-seen states.
Consider a linear sequence of N screens with Next and Back buttons (only one button at each end).
A random tester that presses available buttons uniformly needs an expected $N-1)^2$ presses to reach the far end.

For $N = 10$ , that is 81 presses.
If the tester never revisits a state, the expectation drops to $N - 1 = 9$ — an 81 vs 9 difference.

Thus, a key to efficient scenario-free testing is state deduplication: avoid revisiting.
For the link crawler, treat each URL as a state ID; record visited URLs and skip repeats.
If no natural ID exists, you must add a mechanism to recognize and remember states.

Software Testing: Theory and Practice (Part 6) - Fundamentals of Design for Testability

Kuniwak — Sun, 27 Apr 2025 02:24:54 +0000

Key Takeaways

There are several patterns for achieving a design that is easy to test. This article introduces two representative ones: the SOLID principles and extracting functional components.
To learn design for testability, Test-Driven Development (TDD) is highly recommended.

Overview of Testability

We explained that the heart of shift-left testing is the unit test.
Following the guidance of the test pyramid, you end up writing more unit tests than E2E / integration tests.

However, unit-test cost is heavily affected by the design of the component under test, much more so than with E2E or integration tests.
In a bad example, you might finish the production code in a few hours but spend days writing its unit tests.

Consider the following ImageFetcher, which downloads an image.
Listing 1 shows a version whose unit tests are expensive for two reasons.

Listing 1: An example component with high unit-test cost (TypeScript)

class ImageFetcher {
  // BAD: Uses a global state
  private static readonly cache = new Map<string, Blob>();

  async fetchImage(url: string): Promise<Blob> {
    if (ImageFetcher.cache.has(url)) {
      return ImageFetcher.cache.get(url)!;
    }

    // BAD: The output of fetch cannot be controlled from test code
    const response = await fetch(url);
    if (!response.ok) throw Error(`error: ${response.status}`);

    const blob = await response.blob();
    ImageFetcher.cache.set(url, blob);
    return blob;
  }
}

The first problem is the global cache state.
Because the result of fetchImage changes depending on the cache contents, the order in which tests run influences the outcome, making parallel execution difficult.
You would have to exclude the ImageFetcher tests from your parallel suite.

The second problem is that the fetch response is an indirect input you cannot control.
You would need to spin up an HTTP server that returns an image and tell fetch to hit that URL.

With just a bit of tweaking, we can slash the unit-test cost (Listing 2).

Listing 2: The same code with tweaks that lower test cost

class ImageFetcher {
  // GOOD: cache is now an instance field, not global
  private readonly cache = new Map<string, Blob>();

  // GOOD: fetch can be swapped out for a stub
  constructor(private readonly fetchFunc: (url: string) => Promise<Response>) {}

  async fetchImage(url: string): Promise<Blob> {
    if (this.cache.has(url)) {
      return this.cache.get(url)!;
    }

    const response = await this.fetchFunc(url);
    if (!response.ok) throw Error(`error: ${response.status}`);

    const blob = await response.blob();
    this.cache.set(url, blob);
    return blob;
  }
}

The first tweak moves cache from a global variable to an instance field.
If each test creates its own ImageFetcher, execution order no longer matters and you can run the tests in parallel.

The second tweak lets us inject a replacement for fetch through the constructor.
In tests you can supply a hand-written stub that returns a deterministic response; no need to run an HTTP server.
In production you simply pass the real fetch.

Changing the production design in this way can dramatically lower unit-test cost.
In this series, we will use the term design for testability for designs that keep unit tests cheap to write and maintain.

Design for Testability

There are principles you should follow to achieve testable designs.
Components that adhere to the SOLID principles, for example, are usually easier to test than those that do not.

SOLID Principles and Testability

SOLID principles is an acronym for five design principles:

S – Single Responsibility Principle
O – Open/Closed Principle
L – Liskov Substitution Principle
I – Interface Segregation Principle
D – Dependency Inversion Principle

Single Responsibility Principle

The Single Responsibility Principle states that a component should have exactly one reason to change.
When it is violated, multiple separable concerns become tangled together.

ImageFetcher in Listing 2 breaks this rule: one might change it either to alter HTTP-status handling or to tweak cache behavior.
By splitting it as in Listing 3, you get two components: one interpreting HTTP status codes and one adding caching.

Listing 3: Refactoring Listing 2 to satisfy the Single Responsibility Principle

// Class that interprets HTTP status codes
class ImageFetcher {
  constructor(private readonly fetchFunc: (url: string) => Promise<Response>) {}

  async fetchImage(url: string): Promise<Blob> {
    const response = await this.fetchFunc(url);
    if (!response.ok) throw Error(`error: ${response.status}`);
    return response.blob();
  }
}

// Class that adds caching to ImageFetcher
class CachedImageFetcher {
  private readonly cache = new Map<string, Blob>();
  constructor(private readonly imgFetcher: ImageFetcher) {}

  async fetchImage(url: string): Promise<Blob> {
    if (this.cache.has(url)) {
      return this.cache.get(url)!;
    }

    const blob = await this.imgFetcher.fetchImage(url);
    this.cache.set(url, blob);
    return blob;
  }
}

When concerns are coupled, you typically need more test cases.
If a function with N branches is combined with one with M branches, covering all paths requires M × N cases, whereas separated components need only M + N.
With M = N = 10, that’s 100 versus 20 — a big difference.

Open/Closed Principle

The Open/Closed Principle says components should be open for extension but closed for modification.
A component that violates it forces you to modify existing tests whenever you extend behavior.
One that obeys it lets you keep the old tests unchanged and add new tests only for the new component, lowering maintenance cost.

ImageFetcher from Listing 3 can be extended in an open/closed way.
Suppose you need cache entries to expire after a period.
Instead of editing CachedImageFetcher, add a new ExpirationCachedImageFetcher (Listing 4).

Listing 4: Extending Listing 3 while honoring the Open/Closed Principle

class ExpirationCachedImageFetcher {
  private readonly cache = new Map<string, [number, Blob]>();

  constructor(
    private readonly imgFetcher: ImageFetcher,
    private readonly expirationMs: number
  ) {}

  async fetchImage(url: string): Promise<Blob> {
    if (this.cache.has(url)) {
      const [deadline, blob] = this.cache.get(url)!;
      if (deadline > Date.now()) return blob;
    }

    const blob = await this.imgFetcher.fetchImage(url);
    this.cache.set(url, [Date.now() + this.expirationMs, blob]);
    return blob;
  }
}

Liskov Substitution Principle

The Liskov Substitution Principle requires that instances of a derived type can replace instances of the base type without altering desirable properties.
When satisfied, you can reuse the base type’s unit tests for the derived type, reducing test-development cost.

Interface Segregation Principle

The Interface Segregation Principle says clients should not be forced to depend on methods they do not use.
Violating it makes you supply test stubs for methods irrelevant to the test, increasing boilerplate and effort.

Dependency Inversion Principle

The Dependency Inversion Principle states that high-level components should not depend on low-level components but both should depend on abstractions.
When violated, components often have indirect inputs you cannot control and indirect outputs you cannot observe from tests, pushing you toward expensive, brittle integration tests.

The earlier ImageFetcher that called fetch directly (tagged BAD) violates this principle.
The version that receives fetch from the outside (tagged GOOD) satisfies it.

Want to Dig Deeper?

We have only skimmed the definitions.
For a thorough treatment, consult Agile Software Development: Principles, Patterns, and Practices ¹.

Separating State and Testability

Designing a system so that functional components are separated from stateful ones also improves testability.
A functional component, by definition, returns the same output for the same input.
As noted in Part 1, its behavior can be represented as an input/output table.
Non-functional components are reactive.

Unit-testing reactive components is generally more expensive because you must coerce them into specific internal states.
By isolating stateless functional parts, at least those parts become cheap to test.

Consider FizzBuzzCounter (Listing 5), which increments a counter and prints the FizzBuzz result:

Listing 5: The FizzBuzzCounter class

// Reactive component
class FizzBuzzCounter {
  private mutableCount = 0;

  constructor(private readonly printer: Printer) {}

  get count(): number {
    return this.mutableCount;
  }

  increment() {
    this.mutableCount++;
    if (this.count % 3 === 0 && this.count % 5 === 0) {
      this.printer.print("FizzBuzz");
    } else if (this.count % 3 === 0) {
      this.printer.print("Fizz");
    } else if (this.count % 5 === 0) {
      this.printer.print("Buzz");
    } else {
      this.printer.print(this.count.toString());
    }
  }
}

const counter = new FizzBuzzCounter(new Printer());
counter.increment(); // prints 1
counter.increment(); // prints 2
counter.increment(); // prints Fizz

Unit-testing FizzBuzzCounter is costly: you must call increment at least 15 times to see "FizzBuzz".

You can refactor it into a purely reactive counter, a functional fizzBuzz function, and a display component (Listing 6).
Only fizzBuzz is functional, so it is trivial to test.

Listing 6: Decomposing into more testable components

// Reactive component that only counts
class Counter extends EventTarget {
  private _count = 0;

  get count(): number {
    return this._count;
  }

  increment() {
    this._count++;
    // Notify listeners of the state change
    this.dispatchEvent(new Event("change"));
  }
}

// Component that prints FizzBuzz whenever the counter changes
class FizzBuzzDisplay {
  private readonly handleChange: () => void;

  constructor(private readonly counter: Counter, printer: Printer) {
    this.handleChange = () => {
      printer.print(fizzBuzz(counter.count));
    };
    counter.addEventListener("change", this.handleChange);
  }

  dispose() {
    this.counter.removeEventListener("change", this.handleChange);
  }
}

// Functional FizzBuzz
function fizzBuzz(count: number): string {
  if (count % 3 === 0 && count % 5 === 0) {
    return "FizzBuzz";
  } else if (count % 3 === 0) {
    return "Fizz";
  } else if (count % 5 === 0) {
    return "Buzz";
  } else {
    return count.toString();
  }
}

const counter = new Counter();
const display = new FizzBuzzDisplay(counter, new Printer());

counter.increment(); // prints 1
counter.increment(); // prints 2
counter.increment(); // prints Fizz

How to Acquire Design-for-Testability Skills

While we have introduced patterns for testable design, applying them consciously in practice is surprisingly hard.
You need deliberate training, and Test-Driven Development (TDD) is an excellent exercise.

TDD is a development process where you write the test before the implementation — the so-called test-first approach — and iterate through refactoring (Figure 1).

Figure 1: Process of TDD

Because tests come first in TDD, you cannot write code that is difficult to test; the process forces you to discover testable designs.
Think of TDD as a brace that keeps you in a design-for-testability posture.

Start with a small codebase.
In a large one, finding a testable design is far more difficult and discouraging.
After you gain confidence, tackle bigger legacy systems — Working Effectively with Legacy Code ² is invaluable here.

You can tighten the brace further by avoiding mock libraries and DI containers.
Hand-write test doubles as needed and pass dependencies explicitly.
This motivates you to keep components small and simple.

Eschewing DI containers also discourages tests from depending on knowledge of indirect dependencies ³.
When tests rely on such knowledge, implementation details leak into the tests and you risk false positives where tests fail even though the implementation meets the spec.

Treat TDD as training wheels.
Once design-for-testability has become second nature, feel free to take them off and adjust your development speed to the situation.

Summary

Several patterns help you design code that is easy to test. We covered two major ones: the SOLID principles and extracting functional components.
To learn design for testability, practice Test-Driven Development.

Agile Software Development, Principles, Patterns, and Practices — Robert C. Martin ↩
Michael C. Feathers ↩
Better known as the Law of Demeter. ↩

Software Testing: Theory and Practice (Part 5) - How to Select Test Cases

Kuniwak — Sat, 26 Apr 2025 07:00:44 +0000

Key Takeaways

There are several approaches to sampling a specification.
In this article we introduce two:

A boundary-value approach (On–Off Point method)
A property-based testing approach

Methods for Sampling a Specification

In previous installments we explained that confirming “the implementation satisfies the specification” often requires an enormous—frequently infinite—number of test cases.
In practice, rather than checking every possible case, we sample the specification, verify behaviour for only a very small subset, and infer behaviour for the rest.
Ways to sample a specification are also called test design techniques, and many techniques have been proposed.

This article introduces the boundary-value approach and the property-based testing approach¹.

Boundary-Value Approach (On–Off Point Method)

The boundary-value approach, Boundary-Value Analysis (BVA), selects inputs called boundary values as samples of the specification.
A boundary value is an input at which the branch executed by the hypothetical implementation changes when it contains conditional statements such as if or switch.
Experience tells us that many defects lurk at boundary values. A typical example is confusing x < y with x ≤ y or vice versa.
In such cases the outputs of x < y and x ≤ y differ only when x = y (here “=” means equality, not assignment). The input satisfying x = y is exactly the boundary value.

Certain assumptions must hold for the boundary-value approach to work as intended.

1. The hypothetical implementation has a top-level conditional branch and is followed only by simple processing that contains no loops or recursion. For example, the function isAdult in Code 1, which takes a non-negative age and returns true if the age is an adult and false otherwise, is a typical case.

Code 1. Hypothetical implementation of isAdult, which determines adulthood

function isAdult(age: number): boolean {
  // NOTE: Written verbosely for clarity instead of “return 20 <= age”
  if (age < 20) return false;
  return true;
}

Placing this assumption keeps the number of samples required for testing to a feasible size.
Conversely, when the processing includes recursion or loops, infinitely many boundary values arise, making it impractical to analyse them all.

What does it mean for “infinitely many boundary values to arise”? Let us examine a counter-example that violates the first assumption. Code 2 shows the hypothetical implementation of a function that returns the i-th Fibonacci number for inputs i that satisfy the pre-condition i ≥ 0.
Like Code 1, it begins with conditional branches, but because it contains recursion afterward, it does not satisfy assumption 1.

Code 2. Hypothetical implementation of a Fibonacci function

function fibonacchi(i: number): number {
  if (i === 0) return 0; // branch for i = 0
  if (i === 1) return 1; // branch for i = 1
  // branch for i ≥ 2; contains recursion
  return fibonacchi(i - 1) + fibonacchi(i - 2);
}

It is easy to see that i = 0 and i = 1 are boundary values, but there are actually boundary values hidden in the recursive part for i ≥ 2.

Consider Code 3, which expands the recursion in Code 2 by one level.
You can see that i = 2 and i = 3 are also boundary values.

Code 3. One-level expansion of the recursion in the Fibonacci function

function fibonacchi(i: number): number {
  if (i === 0) return 0; // branch for i = 0
  if (i === 1) return 1; // branch for i = 1

  // expansion of fibonacchi(i - 1)
  let left: number;
  if ((i - 1) === 0) left = 0;      // branch for i = 1
  else if ((i - 1) === 1) left = 1; // branch for i = 2
  else left = fibonacchi((i - 1) - 1) + fibonacchi((i - 1) - 2);

  // expansion of fibonacchi(i - 2)
  let right: number;
  if ((i - 2) === 0) right = 0;     // branch for i = 2
  else if ((i - 2) === 1) right = 1; // branch for i = 3
  else right = fibonacchi((i - 2) - 1) + fibonacchi((i - 2) - 2);

  return left + right;
}

If you continue unfolding processing that contains recursion or loops in this way, you see boundary values proliferate without bound. Hence assumption 1 is introduced so that the sample size remains manageable.

2. Every conditional expression (the part that decides the branch of an if) in the hypothetical implementation is a linear inequality, or a logical OR, AND, or NOT of linear inequalities. Examples that satisfy this condition are x = 0, 0 < x, 0 ≤ x && x < 100, and x = 0 || y = 0. An example that does not satisfy it is i % 3 === 0.

Boundary Defects

As stated above, many defects lurk at boundary values. Such defects are called boundary bugs.
For example, writing x ≥ 0 where x > 0 is required introduces a boundary bug.

When the conditional expression is a single linear inequality and only one variable is involved, four kinds of boundary bugs are possible²:

Shifted boundary – e.g. writing x > 0 instead of x > 1
Closure defect – e.g. writing x ≤ 0 instead of x < 0
Missing boundary – forgetting to branch where a boundary should exist
Extraneous boundary – introducing a branch where none is needed

To uncover all four types, we select, for every boundary in every conditional branch of the implementation,

an input exactly on the boundary, and
the nearest input on either side of that boundary.

Put differently, we “pick the two closest values that lead to different processing”.
This is Boundary-Value Analysis (the On–Off Point method).

Applied to the earlier isAdult function, boundary-value analysis means testing the cases where age is 19 and 20.

Property-Based Testing

We explained that boundary-value testing requires assumptions about the component’s implementation.
Components that violate those assumptions cannot be tested this way.
For such components I recommend adopting Property-Based Testing (PBT).

We have mentioned PBT in prior installments, but here is a refresher. In traditional Example-Based Testing (EBT), humans choose the inputs.
In contrast, PBT automatically generates inputs. The human supplies a relationship that must hold between input and output, and the output is checked against it.
This relationship is typically a post-condition³. For the FizzBuzz function, for example, we might give the following post-conditions:

If the input is divisible by both 3 and 5, the result is "FizzBuzz".
If the input is divisible by 3 but not 5, the result is "Fizz".
If the input is divisible by 5 but not 3, the result is "Buzz".
If the input is divisible by neither 3 nor 5, the result is the decimal representation of the input.

Implementing the first case as a rudimentary property-based test yields Code 4⁴.

Code 4. A naive property-based test for the fizzBuzz function

describe("fizzBuzz", () => {
  context("when the input is divisible by both 3 and 5", () => {
    it("returns \"FizzBuzz\"", () => {
      // collect failing inputs (counter-examples) here
      const counterexamples = [];

      for (let i = 0; i < 100; i++) {
        // mechanically generate multiples of 3 and 5
        const x = Math.floor(Math.random() * 10000) * 3 * 5;

        // if the output is not "FizzBuzz", add x to counterexamples
        if (fizzBuzz(x) !== "FizzBuzz")
          counterexamples.push(x);
      }

      // expect counterexamples to be empty
      assert.deepStrictEqual(counterexamples, []);
    });
  });

  // ... (other cases)
});

The loop tries 100 inputs, and it is easy to increase or decrease that number, so PBT lets us test far more inputs than traditional example-based tests.

However, the automatically generated inputs often fail to satisfy conditions we actually want—most commonly, the pre-conditions.
There are two approaches to eliminate such unwanted inputs:

Implication approach
Custom generator approach

Implication Approach

As explained in Part 2, implication is a logical operator that takes two formulas.
It is written “left ⇒ right” (some people use a double arrow).
Its truth table is shown in Table 1.

Table 1. Truth table of implication

Value of left	Value of right	Value of left ⇒ right
False	False	True
False	True	True
True	False	False
True	True	True

The key point is that the implication is true whenever the left side evaluates to false.

In this approach we put on the left side a formula that returns true for the desired inputs and false otherwise, and we put the test on the right side (Code 5).
For instance, if we wish to treat inputs divisible by 5 as invalid, we can set the left formula to x % 5 === 0. Whenever the pre-condition is false, the entire implication evaluates to true, so the PBT always “passes.”

Code 5. Implementation using implication

describe("fizzBuzz", () => {
  context("when divisible by 3 but not by 5", () => {
    it("returns \"Fizz\"", () => {
      // collect failing inputs (counter-examples) here
      const counterexamples = [];

      for (let i = 0; i < 100; i++) {
        // mechanically generate multiples of 3
        const x = Math.floor(Math.random() * 10000) * 3;

        // if also divisible by 5, treat as pass (the implication’s left side is false)
        if (x % 5 === 0) continue;

        // if the output is not "Fizz", add x to counterexamples
        if (fizzBuzz(x) !== "Fizz")
          counterexamples.push(x);
      }

      // expect counterexamples to be empty
      assert.deepStrictEqual(counterexamples, []);
    });
  });
});

This method is easier than writing a generator and works without relying on any library.
However, because outputs are not checked for inputs that do not satisfy the desired conditions, the actual number of evaluated samples can be smaller than intended.
A serious problem arises when all mechanically generated inputs violate the pre-condition. This situation is called a vacuous truth (often simply vacuous).
If the inputs are vacuous, nothing is really tested. Therefore, when using implication, we should confirm that the generated inputs are not vacuous.

Some PBT libraries offer a filter function that redraws until it finds a sample that makes the predicate true, and they treat vacuous results as test failures.
If available, such filter facilities should be used to avoid vacuity.

Custom Generator Approach

You can also implement your own generator. In PBT libraries, a generator is a component that automatically produces inputs.
When nothing is specified, most libraries choose a default generator that produces arbitrary values of the given type.
If the standard generator produces unwanted inputs, replace it with another generator that yields only the desired ones.

For instance, fast-check⁵, a property-based testing library for JavaScript, allows you to implement a generator by combining existing ones, as in Code 6.

Code 6. Implementation using a generator

import fc from "fast-check";

describe("fizzBuzz", () => {
  context("when divisible by both 3 and 5", () => {
    // generator that produces positive integers divisible by 3 and 5
    // fc.nat() generates naturals; multiply by 3 and 5 to ensure divisibility
    const gen = fc.nat().map((n) => n * 3 * 5);

    it("returns \"FizzBuzz\"", () => {
      // fc.assert throws if it finds a counter-example
      fc.assert(fc.property(gen, (n) => {
        // n is a value generated by gen

        // return true for success, false for failure
        return fizzBuzz(n) === "FizzBuzz";
      }));
    });
  });
});

Finally, a brief note on writing your own generator. A generator for directed acyclic graphs (DAGs), for example, cannot easily be expressed as a combination of existing generators.
One way is to start with an empty graph and repeatedly add either

a node with no parents, or
a new node whose parents are one or more existing nodes chosen at random.

We omitted Equivalence Class Partitioning (ECP). Many definitions of ECP lack theoretical grounding, and those that do have a proper basis are too intricate to explain here. ↩
These are the one-dimensional cases. In two dimensions, boundary tilt is added to the list (Software Testing Techniques, 2nd Edition, Boris Beizer). ↩
When the post-condition cannot be stated succinctly, we sometimes give simpler relationships. For instance, the post-condition for addition over naturals is cumbersome to express explicitly; instead, we often supply multiple simpler laws such as commutativity (swapping the first and second operands leaves the result unchanged). ↩
The code examples below are intentionally simple and eschew libraries. In practice you would use a dedicated PBT library. ↩
https://fast-check.dev/ ↩

Software Testing: Theory and Practice (Part 4) - Fundamentals and Strategies of Unit Testing

Kuniwak — Sat, 26 Apr 2025 01:50:35 +0000

Key Takeaways

In this series, unit testing refers to replacing a component’s dependencies with test doubles.
Test doubles enable the test to control indirect inputs and observe indirect outputs.
For reactive systems, we introduce three approaches: pursuing 0-switch coverage, property-based testing, and model checking.

Unit Testing—The Heart of Shift-Left Testing

The test pyramid ¹ is a well-known guideline that prescribes how many test cases should exist at each stage of the testing process.
The lower the level of coupling, the more test cases you write.
In practice, that means more component (integration) tests than end-to-end tests, and even more unit tests than component tests.
Visualize unit tests as the base of the pyramid and E2E tests as its tip.
Following this guideline yields fast, stable ² feedback.

What Exactly Is a Unit Test?

The term “unit test” is notoriously ambiguous.
Some recent testing books avoid the muddled “unit vs. integration” dichotomy altogether and classify tests by test size instead.
That detour aside, in this series a unit test is defined as a test that targets a single component while replacing its other dependencies with test doubles ³.

In a purely functional language, a component is a single function; in an OO language, it is a single class.
The more components you combine, the larger the state space becomes and the harder it is for people to understand the resulting spec and implementation.
Because a unit test lives at the boundary between a component’s spec and its implementation, once either side grows complex, diagnosing failures becomes painfully time-consuming.
Keeping both spec and implementation small enough for humans to grasp is therefore the driving motivation behind unit tests.

Another major benefit is speed: less code executes, so the tests run faster.

A weakness of unit tests is that they cannot detect integration bugs—failures caused by inconsistencies between components’ specs.
Suppose component A expects an integer while component B returns the integer’s string representation.
Each component individually satisfies its own spec, yet wiring them together causes a type error.
A unit test would never see this.

We said unit tests replace dependencies with test doubles. Why?
To answer that we need the notion of indirect input/output.

Unit Tests and Indirect I/O

Indirect input: input obtained via a dependency rather than a parameter.
Indirect output: output sent to a dependency rather than returned.

Together they are indirect I/O.

We will look at examples, starting with a component that has no indirect I/O.

A Straightforward Component with No Indirect I/O

The familiar FizzBuzz function takes its input as a parameter and returns its output—nothing else.
Hence it has no indirect I/O.

function fizzBuzz(input: number): string {
  if (input % 3 === 0 && input % 5 === 0) return "FizzBuzz";
  if (input % 3 === 0) return "Fizz";
  if (input % 5 === 0) return "Buzz";
  return input.toString();
}

Testing it is trivial; no test doubles are needed:

describe("fizzBuzz", () => {
  context("when given a multiple of 3 and 5", () => {
    it("returns FizzBuzz", () => {
      const actual = fizzBuzz(15);
      assert.strictEqual(actual, "FizzBuzz");
    });
  });
});

A Component with Indirect Input

Indirect input is data a component fetches from a dependency, not from its parameters—current time, random numbers, database queries, etc.
In the greet function below, Clock#getHour supplies the indirect input:

function greet(): string {
  const hour = new Clock().getHour();
  if (hour < 5)  return "Good evening!";
  if (hour < 12) return "Good morning!";
  if (hour < 18) return "Good afternoon!";
  return "Good evening!";
}

Because the test cannot dictate the time, it cannot predict the expected output.
Enter the test stub: a fake that injects tester-specified indirect input.

First, refactor so that a Clock can be injected:

class Greeter {
  constructor(private clock: Clock) {}

  greet(): string {
    const hour = this.clock.getHour();
    if (hour < 5)  return "Good evening!";
    if (hour < 12) return "Good morning!";
    if (hour < 18) return "Good afternoon!";
    return "Good evening!";
  }
}

Now the test can supply a stub clock:

describe("greet", () => {
  context("in the morning", () => {
    it("returns Good morning!", () => {
      const stub = new StubClock({ hour: 9 }); // always returns 9
      const actual = new Greeter(stub).greet();
      assert.strictEqual(actual, "Good morning!");
    });
  });
});

A Component with Indirect Output

Indirect output is data sent to a dependency—writing to a DB, file, etc.
To observe it, we use a test spy that records what was sent.

function writeHelloWorld(file: File) {
  const message = "Hello, World!";
  file.write(message);
}

Testing it with a spy:

describe("writeHelloWorld", () => {
  it("writes Hello, World! to the file", () => {
    const spy = new SpyFile();
    writeHelloWorld(spy);
    assert.strictEqual(spy.content, "Hello, World!");
  });
});

SpyFile stores whatever is written, so the test can assert against spy.content.

Components with Both Indirect Input and Output

Sometimes a component has both.
A single test double would then need to both control indirect input and observe indirect output, making it bulky.
Designs such as CQS (Command-Query Separation) help avoid this by ensuring a component has only one or the other.
We will revisit CQS later in the series.

Beware Overusing Test Doubles

Stubs and spies add lines and can obscure intent.
If you can avoid them—e.g., accept parameters instead of using a stub, return a value instead of writing to a spy—do so.
Whenever you feel compelled to use one, ask whether indirect I/O is truly necessary ⁴.

Unit Testing Reactive Systems

All previous examples were functional: outputs depend solely on inputs.
Reactive systems instead change state in response to interactions.

Consider a Flag that flips its boolean state when toggle is called (see code 8 and figure 1).

class Flag {
  private state = false;

  get isEnabled() {
    return this.state;
  }

  toggle() {
    this.state = !this.state;
  }
}

Figure 1: State-transition diagram of Flag

Tests might look like this:

describe("Flag", () => {
  context("before any toggle", () => {
    it("isEnabled is false", () => {
      const flag = new Flag();
      assert.strictEqual(flag.isEnabled, false);
    });
  });

  context("after one toggle", () => {
    it("isEnabled is true", () => {
      const flag = new Flag();
      flag.toggle();
      assert.strictEqual(flag.isEnabled, true);
    });
  });

  context("after two toggles", () => {
    it("isEnabled is false", () => {
      const flag = new Flag();
      flag.toggle();
      flag.toggle();
      assert.strictEqual(flag.isEnabled, false);
    });
  });
});

That covers three scenarios: 0, 1, and 2 toggles.

Reactive systems often have vast or infinite test-case spaces, so various strategies exist to tame them.
We outline three.

0-switch coverage: Test every direct state transition.
Flag has three: initial → false, false → true, and true → false.
Our tests above already achieve 0-switch coverage.
Property-based testing: Programmatically generate many sequences of calls and assert a property holds for all.
A sketch:

// A naive implementation without a library—use a real PBT library in practice.
describe("Flag", () => {
    it("isEnabled is false after an even number of toggles, true otherwise", () => {
        const counterexamples: number[] = [];

        for (let i = 0; i < 100; i++) {            // try many inputs
            const count = Math.floor(Math.random() * 10000); // random length

            const flag = new Flag();
            for (let n = 0; n < count; n++) flag.toggle();

            if (flag.isEnabled !== (count % 2 === 1))
                counterexamples.push(count);
        }

        assert.deepStrictEqual(counterexamples, []);
    });
});

Model checking: Exhaustively explore states to detect deadlocks or assertion violations ⁵. A deadlock is a state with no outgoing transitions ⁶; an assertion violation is an exception thrown by an embedded assert. Model checking is powerful but abstract, making results harder to interpret than 0-switch tests. (A full code sample would require an external model checker, so it is omitted.)

Summary

In this series, a unit test replaces a component’s dependencies with test doubles.
Test doubles let tests control indirect inputs and observe indirect outputs.
For reactive systems, we discussed three approaches: 0-switch coverage, property-based testing, and model checking.

Some prefer the test trophy, which argues that if component tests can run as fast as unit tests, you should write more component tests than unit tests. ↩
Stable means repeated runs of the same test always yield the same result (pass or fail). ↩
This definition does not draw a sharp line between unit and integration tests. In practice, you rarely stub every dependency—simple utility functions inside the component are usually left real. Conversely, integration tests may employ some doubles. The distinction is therefore gradual, based on how many dependencies are replaced. ↩
We will revisit this in a later article about design for testability. ↩
More formally, model checking also includes verifying temporal-logic properties and refinement relations. ↩
Strictly speaking, you must exclude normal termination states; although they also lack outgoing transitions, they are not considered deadlocks. ↩

Software Testing: Theory and Practice (Part 3) - The Significance and Strategy of Shift-Left Testing

Kuniwak — Fri, 25 Apr 2025 00:19:29 +0000

Key Takeaways

Shift-left testing is a strategy that changes the development process so that defects are discovered earlier.
The earlier a defect is detected, the lower its typical cost to fix.
Detecting defects earlier requires running whatever tests are feasible at each stage as frequently as possible.
ODC analysis lets you inspect and improve your shift-left testing efforts.

Why Shift-Left Testing Matters

Shift-left testing is a strategy that moves the activities for finding defects—including testing—into earlier phases of the development process. Doing so is said to reduce the cost of fixing those defects.
It is called shift-left because timelines are usually drawn left-to-right; moving testing earlier means moving it leftward.

Shift-left testing assumes the empirical rule of thumb that the sooner a defect is found, the cheaper it is to fix. Numerous sources cite that rule, but the evidence is mixed: some publications support it ¹², while others report that the effect appears in some projects but not in others ³.

Even though the rule is not rock-solid, the author believes—based on experience and the four reasons below—that the trend is real.

The shorter the time between defect injection and detection, the fewer unrelated changes are made in the meantime. The search space is smaller, so the fix costs less.
When a defect is found shortly after it is introduced, the code has usually not yet been handed to other developers or testers; the original author can fix it alone, avoiding communication overhead.
If a faulty component is used by other components before it is repaired, those users must also be fixed later. Catching the defect before any downstream code is written avoids cascading rework.
Early detection shortens the overall project timeline. Figures 1 and 2 show Gantt charts for processes that discover defects at different times.

Figure 1: Gantt chart of a process where developers do not test and rely on dedicated testers

Figure 2: Gantt chart of a process where developers test their own work

In Figure 2, developers can fix defects while development proceeds in parallel, shortening the idle time that blocks others in Figure 1. Viewed globally, the lead time from project start to release is shorter, and shorter lead times mean lower costs.

Throughout this series we will proceed on the premise that finding defects earlier tends to reduce the cost of fixing them.

How to Achieve Shift-Left Testing

To shift left, move verification activities as far upstream as possible so that defects surface sooner. That, in turn, means running all feasible checks at every stage.

Table 1 summarizes typical verification techniques and the kinds of defects they can reveal (some are not “tests” in the narrow sense).

Table 1: Examples of defects each stage can uncover

Verification technique	Representative defects it can detect
Syntax highlighting	Syntax errors
Static analysis (simple lint checks)	Variable mix-ups, incorrect API usage, etc.
Static checking (type checking)	Type mismatches, wrong argument lists, etc.
Unit testing	Violations between component spec and implementation, e.g., wrong branch conditions
Integration testing	Spec mismatches between integrated components
E2E / system testing	Spec mismatches across the whole system
Tester-driven verification	Implementer misinterpretations of the spec
Failure monitoring	Defects missed by tests, spec flaws in unusual environments
Customer reports	Defects missed by monitoring, usability problems, etc.

Crucially, no single technique finds every defect and does so immediately.

Earlier stages detect problems sooner but miss some kinds of issues; later stages catch more kinds of issues but only after a longer delay. You therefore need a blended strategy: catch what you can early, and rely on later stages for the rest. The difference becomes clearer in a simulation.

Let’s Simulate

Figures 3–6 arrange common verification stages from earlier (top) to later (bottom). For a given defect, draw an arrow downward; the arrow stops at the stage where the defect is caught (Figure 3).

Figure 3: How to read the simulation diagrams (1)

If we have two defects caught at different stages (Figure 4), the arrow that stops higher up represents a defect found earlier—and therefore cheaper to fix—than the arrow that stops lower down.

Figure 4: How to read the simulation diagrams (2)

Now compare two development styles. One uses a language without static type checking, edits code in a plain text editor, and developers do no self-testing (Figure 5). The other uses a statically typed language, an IDE-like environment, and developers test their own code (Figure 6).

Figure 5: Process with plain text editing and no developer-run checks

Figure 6: Process with an IDE-like environment and developer-run checks

The latter clearly finds defects earlier, hence at lower cost. That illustrates why running every feasible test as soon as it becomes feasible is worthwhile.

Note that we have discussed only a subset of defect-detection activities. Defects can also be introduced during requirements analysis, specification, and design; shift-left should target those phases too. ⁴

For example, during specification you can build a working throwaway model (a prototype) and exercise it in limited scenarios to uncover spec defects early. Paper sketches, design-tool prototypes (Figma ⁵, Sketch ⁶, Zeplin ⁷, etc.), even block toys plus a camera for 3-D game terrain—any medium is fine as long as it answers the questions you have.

Writing the spec in a rigorously defined language (formal specification) also exposes unintended ambiguity early, as explained in Part 2. Taken together, these early activities enable shift-left testing.

But teams often leave shift-left opportunities undiscovered. How can you spot them? One answer is ODC analysis.

ODC Analysis

ODC analysis (Orthogonal Defect Classification) classifies every detected defect along four independent attributes: type, trigger, source, and impact (Table 2).

Table 2: The four ODC attributes

Attribute	Meaning
Type	Root cause category—e.g., wrong or missing configuration, incorrect comparison, etc.
Trigger	Process that revealed the defect—code review, unit test, E2E test, and so on
Source	History of the faulty component—new, reused, modified, third-party, etc.
Impact	Kind of failure effect—usability, performance, reliability, deployability, etc.

Suppose an E2E test of a web app finds that a page fails to open when the user name is null, due to missing SQL escaping. The type is “missing functionality,” and the trigger is “E2E test.” Recording that information for every defect enables multifaceted analysis.

For shift-left purposes we focus on type and trigger. From type we infer the stage where the defect should have been caught; from trigger we see where it was caught. If actual detection lags behind expectation, we revise the process. After running with the revised process for a while, we perform ODC analysis again to verify that detection has indeed shifted left. Thus ODC provides both insight for improvement and a way to measure the effects of process changes.

Capers Jones, Applied Software Measurement: Global Analysis of Productivity and Quality, McGraw-Hill, April 2008. ISBN 978-0-07-150244-3 ↩
Karl Wiegers & Joy Beatty, Software Requirements, 3rd ed., Microsoft Press, 2013. ISBN 978-0-7356-7966-5 ↩
Tim Menzies, William Nichols, Forrest Shull & Lucas Layman, “Are delayed issues harder to resolve? Revisiting cost-to-fix of defects throughout the lifecycle,” Empirical Software Engineering 22 (4), 2017, 1903–1935. https://doi.org/10.1007/s10664-016-9469-x ↩
In Parts 1 and 2 we defined a defect narrowly as “an input that makes implementation and specification disagree.” Here we use a broader definition: “an input that violates correctness or validity,” so that requirement and specification problems also count as defects. ↩
https://www.figma.com/ ↩
https://www.sketch.com/ ↩
https://zeplin.io/ ↩

Software Testing: Theory and Practice (Part 2) - Software Testing and Logical Expressions

Kuniwak — Wed, 23 Apr 2025 23:41:03 +0000

Key Takeaways

The conditions we need to check when testing functional programs can be expressed as logical formulae.
Make it a habit to think about specifications and software tests in terms of logical expressions.

Recap of Functional Program Testing from Part 1

In this second installment we re-explain Part 1 from a different angle, so let’s quickly review:

A functional program’s specification can be described as a table mapping some inputs to outputs, and the implementation’s meaning as a table mapping all inputs to outputs.
If, for every input listed in the specification, the output matches the implementation’s table, then the implementation satisfies the specification.

These explanations are in fact natural-language translations of concepts originally described as logical formulae in computer-science literature.
The goal of Part 2 is to let you understand those original formulae.

Trying to explain logical notation without motivation can feel unsatisfying, so let’s first see why it is worth using.

Why Logical Expressions?

Behind specifications, implementations, semantics and software tests lies an important concept: verification of correctness.
In the sources we introduced, the core of verification is always described with logical formulae.
Why did the authors choose formulae instead of plain language?

There are two reasons:

Natural language is ambiguous; one description may admit multiple interpretations.
Logical notation makes it much easier to check the validity of an argument.

Consider the ambiguous sentence “I saw the man with the telescope.” — who has the telescope?
When explanations allow multiple readings, different people may derive different conclusions.

To avoid such tragedies we should use a language whose meaning is as precise as possible, and logical notation is a well-known candidate.

Of course formulae cannot eliminate every misunderstanding: a reader may misread symbols, or fail to map them to real-world concepts. Nevertheless, they cause far fewer misinterpretations than plain language.

The field that studies logical expressions is symbolic logic. Its literature covers both the meaning of formulae and formal proofs built from them — which brings us to the second advantage.

With logical proofs, if you can start from known formulae and reach your claim by following the prescribed rules, your claim is proven correct.

In short, plain language is ambiguous and makes validity hard to check. For critical core ideas that we do not want misread, authors use logical expressions.

Both Part 1 and Part 2 of this series are examples of that approach. For each step we:

Formulate an explanation as a logical expression that reduces the gap to traditional software-testing concepts.
Verify that this expression follows from the literature’s formulae by a valid proof.
Translate the expression into natural language.

Step 2 lets the author confirm the translation’s correctness precisely ¹ — a task that would be much harder had step 1 not been written as formulae.

Because natural-language premises can be interpreted in multiple ways, judging the soundness of an argument written in plain text is hard. If both premises and conclusion are formulae, you only need to check that the premises hold and the proof follows the rules to be confident in the conclusion.

Sidebar: Specifications as Logical Formulae

Naturally, precise logical expressions can describe program specifications themselves.

If implementer and verifier interpret a spec differently, they are effectively working on different programs. Successful testing then becomes unlikely, leading to re-work, extra costs and delays.

Specification notation must fit the system’s domain. Different notations carry different overheads and mitigate re-work to different degrees.
For domains where errors after deployment are extremely costly (aerospace, medical, rail, finance), formal logic or specialised spec languages are often worth the effort. For a small e-commerce site or a game, that cost may be overkill.

Meaning of Logical Expressions

Now that we know why we use formulae, let’s learn just enough notation to follow Part 2. A comprehensive treatment would fill a textbook, so we’ll cover only what we need.

What Is a Logical Expression?

A logical expression (or formula) is a string of symbols conforming to a fixed grammar.
Examples: P ∧ Q, ∃x. ∀y. (R x y) ².

Below we introduce just the constructs needed to understand testing-related formulae. For deeper study, see an introductory logic text.

Building Blocks

Conjunction (logical AND)

P ∧ Q (“P and Q”) is true iff both P and Q are true.

Table 1: Truth table for conjunction

Left	Right	Result
T	T	T
T	F	F
F	T	F
F	F	F

Programmers can think of && / and.

Implication

P ⟶ Q (“if P then Q”) is false only when P is true and Q is false; otherwise true ³.

Table 2: Truth table for implication

Left	Right	Result
T	T	T
T	F	F
F	T	T
F	F	T

A chain P ⟶ Q ⟶ R parses as P ⟶ (Q ⟶ R); everything but the rightmost is premise, the last is conclusion.

Predicate

A predicate returns a truth value. P x denotes P applied to x.
E.g. white x is true iff x is white.

Existential quantifier `∃`

∃x. (P x) (“there exists an x such that P x”) is true iff some x makes P x true ⁴.

For instance, ∃x. white_crow x is true because white crows exist.

Universal quantifier `∀`

∀x. (P x) (“for all x, P x”) is true iff P x is true for every x ⁴.

∀x. (crow x ⟶ black x) is false because there are white crows.

Combining ∀ with implication narrows the domain:
∀x. ((crow x) ⟶ (black x)) reads “for all x that are crows, x is black.”

A chain ∀x. ((P x) ⟶ (Q x) ⟶ (R x)) means: for every x, if all premises hold, then R x holds.

That concludes our crash course. We are ready to express testing concepts as formulae!

Logical Formulae for Software-Testing Concepts

An essential notion behind testing is total correctness.
Software testing can be viewed as sampling inputs to find cases where total correctness is false (defects). Part 1 explained specification/implementation in those terms.

Here we use formulae to define total correctness (and its components). We assume functional programs (one deterministic output per input).

What Is Total Correctness?

A program is totally correct iff it both terminates and returns an output listed in the spec for every input that the spec declares valid.

Thus total correctness = termination + partial correctness.
Termination: the program never loops forever on any valid input.
Partial correctness: assuming it does terminate, the output matches the spec.

To state this precisely we introduce:

Pre-condition pre i: whether input i appears in the spec’s table.
Post-condition post i o: whether the pair (i,o) appears in that table.

The Denotation Function

The denotation function denote prog i returns the output of program prog on input i if it terminates; otherwise undefined. Thus denote is a partial function.

With this we can state total correctness precisely.

Formula for Total Correctness

TC pre post prog (“Total Correctness”) means:

For every input satisfying pre, executing prog terminates and the result satisfies post.

Define:

TC pre post prog ≡ (T pre prog) ∧ (PC pre post prog)

where T is termination, PC partial correctness.

Termination Predicate `T`

T pre prog ≡ ∀i. (pre i ⟶ ∃o. (denote prog i = o))

True iff for every valid input i there exists some output o (i.e. prog terminates).

Partial Correctness Predicate `PC`

PC pre post prog ≡ ∀i. ∀o. (pre i ⟶ (denote prog i = o) ⟶ post i o)

True iff for every valid input i, if prog terminates with o, then post i o holds.
Both predicates together yield total correctness.

Translating to Testing

A defect is an input that makes total-correctness false, i.e. violates termination or partial correctness.
Testing samples finite inputs I₁,…,Iₙ approximating the universal quantifiers. For termination:

(pre I₁ ⟶ ∃o. denote prog I₁ = o) ∧
(pre I₂ ⟶ ∃o. denote prog I₂ = o) ∧ … ∧
(pre Iₙ ⟶ ∃o. denote prog Iₙ = o)

Similarly for partial correctness with expected outputs O₁,…,Oₙ.
A good test suite approximates the true quantified formula well with few cases.

Conclusion

By reading these formulae we gain a sharper understanding of software testing, and we can construct convincing formal arguments about correctness.

Here, “confirm” means checking that replacing the literature’s definitions with those used in this series causes no problems; i.e. that the two versions of total correctness are equivalent for the same program and specification (pair of pre- and post-conditions). The book Semantics with Applications defines correctness using operational semantics (fixing an evaluation order), whereas Part 1 did so with denotational semantics (viewing programs as mathematical functions). ↩
Notation follows Isabelle syntax: https://isabelle.in.tum.de. ↩
Some texts write ⇒ instead of ⟶. ↩
Parentheses are redundant; we keep them for readability. ↩

Software Testing: Theory and Practice (Part 1) - Fundamental Concepts of Software Testing

Kuniwak — Wed, 23 Apr 2025 00:31:23 +0000

Purpose of This Series

In this series, we will thoroughly explain basic concepts and best practices related to writing test code, test design, and test strategies in software testing. The intended audience ranges from those who have heard of software testing but don't know what it entails, to those struggling to understand the theoretical aspects of it.

This series includes definitions and explanations of foundational concepts in software testing. Unfortunately, many books on software testing do not clearly define basic terms like "specification" and "behavior." Merely reading vague explanations can create a false sense of understanding, or lead to inconsistent interpretations. This series aims to provide a more solid understanding of software testing based on clear definitions from computer science.

Key Takeaways

Software testing is the process of verifying that the implementation meets the specification.
A specification refers to the expected behavior of a program. If the program determines output based on input, this behavior can be represented as an input-output table.
The purpose of software testing is to confirm that the risk of failure is within acceptable limits, and to prompt fixes if it is not.

Overview of Software Testing

In this series, software testing is succinctly defined as "the process of verifying that the implementation meets the specification"¹. Some literature may include checking whether the implementation meets requirements, but for the sake of clarity, this series adopts the narrower definition.

For example, consider a specification that requires "displaying the name of the logged-in user." If a user registers their name as null or constructor, and the name is not displayed or causes an error, then the implementation fails to satisfy the specification².

In short, the purpose of software testing is to ensure that names like null or constructor do not cause errors, and to determine whether the implementation needs fixing if they do.

To understand software testing more deeply, we must also define the terms "specification" and "implementation." Can you clearly explain what a specification or implementation is? If not, read on for definitions and theory.

Definitions and Theory Surrounding Software Testing

Understanding the definitions of specification and implementation, and the relationship between them, is essential to understanding software testing. Yet, most testing books do not define these terms properly. In engineering disciplines like software testing, definitions are often provided by fundamental sciences like computer science. This section borrows definitions from computer science literature to explain key concepts.

Specification

In computer science, one common definition is:

Generally, the expected behavior of a program is called the program's specification.

A specification is defined as the "expected behavior" of a program. While this seems straightforward, digging deeper often reveals surprising misunderstandings.

Behavior

A key point that varies in understanding is the definition of "behavior." This article focuses on functional programs, where the output is uniquely determined by the input³.

For example, a Fizz Buzz program — outputting "Fizz" for multiples of 3, "Buzz" for 5, and "Fizz Buzz" for both — is functional. A compiler translating source code into machine code is also a functional program.

In functional programs, behavior refers to the relationship between input and output, which can be represented in a table like Table 1. Exceptions can be listed instead of return values.

Table 1: Fizz Buzz Program Specification

Input	Output
1	"1"
2	"2"
3	"Fizz"
4	"4"
5	"Buzz"
6	"Fizz"
7	"7"
8	"8"
9	"Fizz"
10	"Buzz"
11	"11"
12	"Fizz"
13	"13"
14	"14"
15	"Fizz Buzz"
(and so on⁴)	…

Inputs not listed in the table are considered to have implementation-dependent undefined behavior — the implementation can handle them freely. This allows for more efficient or optimized implementations.

However, implementations for undefined behavior have no intrinsic value. Good specifications allow some freedom but avoid sacrificing value⁵.

Returning to the "display logged-in user name" example: a program that displays any logged-in user’s name is correct. If it fails even once or crashes, it does not meet the specification. If the user is not logged in, the spec allows undefined behavior (e.g., an error message).

Aside: Reactive Programs

So far, we’ve covered functional programs, which take input, produce output, and stop. Some programs are reactive — continuously interacting with users or other programs. A web server is one example.

Reactive programs require a different definition of behavior. One formalism for specifying such behavior is Communicating Sequential Processes (CSP), which can also express implementations and automatically verify conformance.

Implementation

An implementation is "a program intended to satisfy a given specification." While not always precisely defined in literature, this is the general usage.

Code 1 will show an example Fizz Buzz implementation, which throws an error for inputs <1.

Code 1: Example Implementation of the Fizz Buzz Program

// Fizz Buzz program implementation written in TypeScript
function fizzBuzz(i: number) {
    if (i < 1 || !Number.isInteger(i)) throw Error('Unsupported input');
    if (i % 3 === 0 && i % 5 === 0) return "FizzBuzz";
    if (i % 3 === 0) return "Fizz";
    if (i % 5 === 0) return "Buzz";
    return i.toString();
}

Unlike specifications, implementations must define output for all inputs. The input-output relationship in implementations is called the meaning of the program and can also be shown in a table (Table 2).

Table 2: Fizz Buzz Program Meaning

Input	Output
<1	Exception
1	"1"
2	"2"
3	"Fizz"
4	"4"
5	"Buzz"
…	…

The implementation satisfies the specification if the meaning (actual output) is included in the specification (expected output). If any output differs, the implementation fails to meet the spec.

Defect

A defect (or bug) is a point where the implementation does not match the specification. Formally, it is an input that produces different output than specified — including exceptions or infinite loops.

Failure

A failure occurs when a defective input is actually executed, and the resulting output differs from the spec. A defect doesn't always cause a failure unless the input is used. But every failure has an underlying defect.

Failure Risk

Failure risk combines severity and probability. Often, severity is rated with integers, and risk is calculated as severity × probability to enable comparison.

With this groundwork, we can better understand the definition and purpose of software testing.

Software Testing

As stated, software testing is verifying that an implementation meets the specification — or confirming the absence of defects.

To verify there are no defects, all possible (often infinite) inputs must be tested. Even for Fizz Buzz, verifying every number ≥1 is required. Reactive programs can have infinite traces even with finite input spaces⁶.

Since exhaustive testing is unrealistic⁷, software testing relies on sampling — selecting testable inputs from the specification.

Testing only samples can't confirm the absence of all defects. Thus, the goal is often adjusted: to verify that failure risk is acceptable.

Even partial testing reduces failure risk compared to no testing. As long as the benefits outweigh the risks, the program has value.

So even if software testing doesn’t prove correctness, it remains highly valuable.

Test Case

A test case is a pair of input and expected output sampled from the specification⁸. For Fizz Buzz, test cases can be extracted from the table (see Table 3).

There are two major approaches:

Example-based testing: selects concrete input-output pairs
Property-based testing: defines relations between inputs and outputs

Property-based testing allows more automatic input generation but requires discovering correct relationships — a more difficult task. Both will be discussed in later parts.

Table 3: Example Fizz Buzz Test Cases

Input	Expected Output
1	"1"
3	"Fizz"
5	"Buzz"
15	"FizzBuzz"

Conclusion

Software testing is the process of verifying that the implementation meets the specification.
A specification refers to the expected behavior of a program. If the program determines output based on input, this behavior can be represented as an input-output table.
The purpose of software testing is to confirm that the risk of failure is within acceptable limits, and to prompt fixes if it is not.

This explanation limits software testing to verification — confirming that the implementation meets the specification. Broader definitions (e.g., from ISTQB or SQuaRE) include validation — confirming that the implementation meets the requirements. ↩
null can cause issues in SQL queries without parameter escaping. constructor is problematic in JavaScript when using objects as dictionaries without hasOwnProperty. ↩
For clarity, we exclude non-deterministic programs like those relying on random numbers or the current time. ↩
Although inputs ≥16 are omitted, they should be specified. Specifications may also be written in natural language or logic. For example: “For input n > 0, if divisible by both 3 and 5, return 'FizzBuzz'; by 3 only, 'Fizz'; by 5 only, 'Buzz'; otherwise, return n as a string.” ↩
If all inputs are undefined, even random outputs or errors satisfy the spec, yet such implementations are worthless. Specifications must balance between freedom and meaningfulness. ↩
Functional programs have finite but huge input spaces. Reactive programs may have infinite traces, even if inputs are finite. ↩
Logical proof tools like Isabelle or Rocq can prove absence of defects even for infinite input spaces. ↩
ISTQB defines test cases more broadly to support reactive programs. ↩

How Implementing a Static Checker for Screen Specifications Led Us to Uncover Numerous Defects

Kuniwak — Tue, 22 Apr 2025 00:00:19 +0000

I’m Kuniwak, a Software Engineer in Test.
In this article I present a case study on developing a static checker for screen specifications (explained below).

What I Want to Share

Specification documents that describe screen layouts and transitions can be made machine‑readable.
Once a specification is machine‑readable, static checking of the spec becomes possible.
By running a static check we uncovered just under 40 defects across 15 % of the screens in my scope of responsibility.
Machine‑readable specifications pave the way for further automation and reuse.

Recap: What Is a Specification?

There are several definitions of specification.
Here, we treat a specification as the criterion that defines the correct behaviour of an implementation.
When an implementation is judged correct, we say that the implementation satisfies the specification.
Regardless of who performs the judgment, the result should be identical.

Just as implementations can be faulty, specifications themselves can contain defects.
If a specification erroneously flags behaviour that was intended to be correct—or the reverse—it is defective.

A classic example is contradictory statements.
If one part of the spec instructs the login‑screen button text to read “Login” while another says “Sign In”, no implementation can satisfy both simultaneously.
A specification that no implementation can satisfy is worthless; evidently some behaviour was supposed to be accepted, but the spec rejects it.

Another kind of defect (outside this article’s scope) arises when the spec is internally consistent yet the resulting correct implementation fails to solve the real‑world problem (e.g. sales targets are still missed).

What Happens When a Specification Has Defects?

In a development process the main consumers of a specification are:

Implementers – responsible for delivering an implementation that satisfies the spec.
Verifiers – responsible for confirming that the implementation satisfies the spec.

If the specification is defective, both suffer:

Unnecessary communication cost
- If implementers or verifiers notice something suspicious, they must raise questions before coding—communication that should have been unnecessary.
Wasted implementation / verification cost
- If no one notices, code is written exactly as specified; the defect surfaces only when spec authors touch the system. Even if caught before release, some or all of that work is wasted.
Loss of trust
- If the defect slips into production, end‑users discover it and confidence is lost in addition to wasted effort.

In short:

A specification is the yardstick for correct system behaviour.
Specifications, like code, can contain defects.
Defective specs cause extra cost and may damage trust.

What Is a Screen Specification?

This article deals with specs about the appearance of GUI screens and the transitions between them.
Together we call these the screen specification, consisting of a screen‑display specification and a screen‑transition specification.

A screen is (roughly) a set of application states grouped by identical GUI appearance ¹.
Take a typical login screen: the states formed by combinations of input‑form contents and server‑communication status collectively make up the login screen.

For instance, if a service distinguishes general and privileged users, their login screens may look alike, yet the paths leading to them and subsequent destinations differ, so modelling them as separate screens is clearer.

State transitions within a screen—or between screens—are triggered by events such as UI actions (click, hover, scroll), server messages, or simply time.

Screen‑Display Specification

Most screens place UI elements such as input forms and buttons at fixed positions.
A screen‑display specification instructs, for each state, where each UI element appears and how it looks.
Behaviour and state changes of individual UI elements are usually defined separately as a UI‑element specification, so shared widgets need not be duplicated across screens.

In this article we assume the UI‑element spec already exists and the screen‑display spec describes:

Layout – where each UI element sits, and
Behaviour caused by interaction between UI elements.

Interaction between UI elements means that an event changes multiple elements in concert ².
Example: an input form and a text label share a screen.
On keyboard input, if the entry violates a rule, an error message appears in the label; otherwise the label is hidden—a textbook UI interaction.

Example

If element positions do not vary by state, a single screenshot suffices to show the layout.

Where layouts differ by state, representative screenshots for each layout suffice.

UI‑element interaction must be described in addition to the layout picture; in this case we use natural language, like the error‑message example above.

An implementation is judged to satisfy the screen‑display spec if, given the same event sequence, its appearance matches the spec in every state ³.

If they are non‑deterministic, each yields a set of possible appearances; the implementation passes when its set is included in the spec’s set.
If internal events exist, unstable states should be excluded. For client–server screens you usually want to expose communication events rather than hide them.

Screen‑Transition Specification

Most GUIs expect users to navigate through multiple screens.
We model a screen’s internal states as nodes and events as labelled directed edges, forming a graph called the screen‑transition specification.

For example, from state S_0 (empty user‑name/password fields) entering correct credentials Foo + password moves to S_Foo; we draw an edge labelled “input valid credentials for Foo” between those nodes ⁴.

Common notations include state‑transition diagrams and tables.

Explaining how to judge conformance to this spec would be lengthy; our implementation relies on the theory of Communicating Sequential Processes (CSP).
For details, see the concept of refinement in CSP.

Making the Screen Spec Machine‑Readable

We started with existing Confluence pages written in Confluence wiki markup that lacked enough detail to serve as screen specs.
We rewrote each screen as a pair of:

a UI‑element layout diagram (left below), and
a UI‑element table (right below).

Scr.001 is the screen ID and Login Screen is the screen name.
Every screen is given an ID because other parts of the spec (e.g. the UI‑element table’s transition column) need to reference screens uniquely.

The left image is part of the screen‑display spec.
The right table records, for each UI element, its ID, type, display conditions, display content, and interactions.
Display conditions/content belong to the screen‑display spec; interactions belong to the screen‑transition spec.

Because the UI‑element table is plain wiki markup, our static checker can parse it to extract the transition graph.
State‑transition diagrams are drawn with a PlantUML macro so they remain machine‑readable.

Static Checking of Machine‑Readable Screen Specs

A machine‑readable spec enables static analysis.
We implemented a static checker (~6000 lines of Go) with 23 rules based on about 20 spec‑inspection viewpoints gathered in advance.
Here are a few examples (eight were automated):

Consistency between the transition diagram and UI‑element tables
- Each edge in the PlantUML diagram must appear in some table’s interaction column, and vice‑versa.
Interaction description for interactive elements (buttons, check‑boxes, etc.).
Explicit ordering for list‑type UI elements (look for the word “order” in the content column).
Scaling instructions for dynamic images (“zoom in/out” or “crop” must appear when image size differs from its frame).
…

However, a fully machine‑readable notation is not always human‑friendly, so we limited ourselves to natural‑language explanations in this case.

To avoid overlooking typos or omissions we added 15 auxiliary checks, e.g.:

No duplicate IDs.
The string TODO must not appear.
Text and images must specify whether they are static or dynamic.
…

Implementation‑wise, each rule is a function that takes one of layout, element table or transition diagram and returns a list of detected defects, keeping rules independent and easy to add/remove.
Ignoring non‑applicable elements prevents imposing a single rigid format; richer notations (e.g. a flowchart for complex conditions) can coexist, and dedicated rules can be added later.

Results of Introducing Static Checking

Using this checker, we caught 40 defects across 15 % of the screens before the spec reached programmers.
After the checker flagged issues, the number of follow‑up questions about the spec was lower than in comparable projects without the checker.

Challenges of Machine‑Readable Screen Specs

Maintaining a machine‑readable spec turned out to be burdensome for non‑programmers, so the checker did not see continuous use.
Handing spec maintenance to developers might solve this, but then their effort must be justified—perhaps by automatically generating part of the implementation from the spec, as discussed next.

Applications of Machine‑Readable Specs

Making the screen spec and its surroundings machine‑readable allows parts of the specification process to be automated.
In our case, steps P3 and P4 of the process flow diagram were automated.
For P3, we linked layout diagrams to Figma objects and used the Figma API to refresh screenshots mechanically ⁵.

With a machine‑readable spec we could also auto‑generate parts of the implementation or of the test suite.
Complete generation may be hard, but partial generation is realistic.
For example, typical E2E tests exercise screen transitions; by adding element IDs to the transition spec, E2E tests could be generated automatically.

One could also imagine an MCP server that indexes and interprets machine‑readable specs for LLMs, aiding code generation, test generation, or other tasks.

Summary

Specification documents describing screen layouts and transitions can be made machine‑readable.
Machine‑readable specs enable static checking.
Static checking uncovered nearly 40 defects across 15 % of the screens in my area.
Machine‑readable specs open the door to further automation and reuse.

Even visually similar pages can be treated as separate screens. ↩
This parallels parallel composition in CSP. ↩
When both spec and implementation are deterministic and contain no internal events. ↩
For clarity, this diagram uses raw states and events. In practice it is cleaner to include state variables, guards and post‑conditions. ↩
Confluence’s Figma‑embed widget was too slow, so we avoided it. ↩