We universally accept that shorter feedback cycles are good—working them in between coding and testing, sprint planning and sprint retro, merging and deployment. But two critical areas lack early feedback: requirements and design. Issues in design are only caught at the implementation level, and issues in the requirements are only caught when you present code to the client. Inevitably, our designs need change, like all first drafts do. But if it takes so long to get feedback on the design, what's the point of designing in the first place?
Requirements are worse. Often, when a client gives us ambiguous or contradictory requirements, we only discover it when we show them our next prototype. It would be so much better if we could come back immediately with the necessary questions, but we don’t. We waste their time and ours on every iteration.
It doesn’t have to be this way. There’s nothing special about designs or requirements that make them impossible to analyze. It’s just that, historically, almost all of our feedback tools are built to analyze code. We never consider requirements or designs as something we can test, too. If we could, we could shorten the feedback cycle on thinking through our code, saving us and our clients a lot of time and money.
The art of writing directly-testable requirements and designs is called formal specification. While it’s been niche for a while, more and more companies are experimenting and succeeding with these techniques. They allow us to deliver higher-quality software cheaper and faster.
Disclaimer: I sell workshops and consulting services for the languages I mention (like I’m gonna turn down a chance to shill to GitHub!).
Overview
The core idea of formal specifications is simple: Create a blueprint of your design, write some properties the blueprint should maintain, and test that you have those properties. From there comes a wide variety of ideas. Just as there are different programming languages for implementing different kinds of projects, there are different specification languages for studying different classes of designs. Alloy, for example, is often used to check that data schemas match business requirements. You might say “policies apply to groups, groups can have subgroups, policies can have sub policies,” and the Alloy tooling will generate diagrams of possible unusual cases you’d need to handle in your project.
sig Group {
, supergroup: lone Group
}
sig Policy {
, superpolicy: lone Policy
, applies_to: Group
}
fact "no cycles" {
no iden & (^supergroup + ^superpolicy)
}
run {} for 2
For something like designing distributed systems, on the other hand, you often see people using TLA+. TLA+ is a specification language for handling the issues of concurrency, such as deadlocks, race conditions, and eventual consistency. It’s also the tool that brought public attention to formal specification, when AWS used it to find a 35-step bug in DynamoDB that passed all their tests and code reviews.
There are other design languages with other tradeoffs, but simply listing a bunch of technologies does not make for a good essay. Instead, let’s take a deep dive into an introductory technique called decision tables. Not only is it effective and widely used in specification, it’s so simple that you’ll be proficient enough to use it yourself by the end of this essay.
Decision tables
Decision tables are a way of specifying choices your system can make in a given context. We take every possible combination of inputs and map each one to a system output. For example, let’s say you’re driving in the United States and want to make a turn at an intersection. There’s a single traffic light in front of you. Can you make the turn?
There are three possibilities for the light color and two turn possibilities, so that’s 3*2=6 rows total. That’s where the formal part of the formal specification comes in: If we don’t have exactly six rows, we immediately know the table is somehow wrong. If there’s a missing row, or two rows that have the same inputs, we also know the table is wrong: There’s an ambiguity or a contradiction, respectively.
Looking at the above table, it doesn’t matter what turn we’re making if the light isn’t red. It’s always okay. So we can simplify the table to show that:
Each row with one dash (-) covers two possibilities, so that’s two red, two yellow, and two green, for 6 total.
And that’s it. Now you know decision tables! Let’s walk through an example of applying it in practice.
An example
Zoom has a “share screen” feature. The host can set three options:
I’m asked to implement a similar feature in a different client. For simplicity, we’ll assume I only need to implement just the first two options, “How many participants can share at the same time?” and “Who can share?” Under what cases can I share my screen?
There are four possible inputs in our decision table:
Can only the host share?
Am I the host?
Is someone else sharing?
Is multishare enabled?
All of these are booleans. Our table then has 2⁴ = 16 rows total. Here’s my first row:
Already, I see something interesting: If only the host is allowed to share, and I’m the host, and someone else is already sharing, what happens? Zoom only lets one person be the host at a time, so the person sharing is not the host. This means something is wrong! More specifically, our feature violated an invariant. Invariants are properties that must always be true in every state of the system. Here, the invariant is
If "only the host can share” is enabled then someone who isn’t the host cannot share.
This may seem obvious from the options, but it’s easy to miss implicit invariants in the stress of work. Making design decisions explicit, versus implicit, means it’s more likely we’ll pay attention. It’s also a good idea to figure out what’s not an invariant in the system, even if it happens to always be true right now. That tells us what we can change later.
Once we consider the invariant, the first row would look something like this:
It doesn’t matter what Multishare is here, because either way we already have a problem. This also encourages me to look for ways the code can potentially break this invariant. For example, what if I enable OnlyHost while someone else is already sharing?
After that, I finish the rest of the table:
That’s 2+2+4+2+2+4 = 16 rows, and all of them are unique. That means there’s no missing rows indicating a missing requirement, and no duplicate rows indicating a requirement contradiction. This doesn’t mean the rows are correct: They might not match up with the intended requirements.
Fortunately, decision tables are easy to read, even by nontechnical people. This means I can share the table with a project manager and they can check it line by line. They’d likely find a problem: I said if multishare is disabled and someone else is sharing, then I can’t share… even if I'm the host! We probably don’t want that. Fixing the table:
With that fix, the table is a complete specification.* I can use it as a reference while developing. I can also use it to generate tests, either manually or via a translation program.
If you’re interested in reading more about decision tables, I’ve written an essay on patterns and technique here.
I like decision tables because they are simple, easy, and powerful. Anybody can learn them in five minutes and use them, even without a technical background. But one thing we didn’t do with them is directly connect the decision table to our code. And this is the main limitation of modern formal specification: There’s no built-in way to guarantee that you faithfully implemented your design. It’s possible, and people have done it, but it takes a lot of hard work to do this.
This is an intentional choice. From experience we know that tools which connect design to code are much, much harder to use, making them less accessible for most programmers. Instead, it focuses on what it is best at: shortening the feedback loop from design to design.
Also, it means the tools aren’t magic. I don’t trust magic.
If you find decision tables useful and want to go deeper with formal specification, I’d recommend starting with Alloy. We’ve recently written new online documentation for it and the official book is fantastic. TLA+ is more complex but can do more powerful things; I also just finished writing new documentation for that, too. You can also check out my website, where I’ve written a bunch of articles on formal specification.
Thanks to Rebeca Carillo and Zack Galvin for feedback on this Guide.
