This is the first installment of a comprehensive course on property-based testing (PBT), a powerful approach to software testing that combines universal properties with random input generation.

Created by Antithesis in collaboration with Carnegie Mellon University’s Center for Transformational Play, this course shows how and why PBT is more effective than conventional methods of software testing, and how PBT can be applied to both single applications and entire production systems.

In this introduction, Alperen Keles (now Senior Software Engineer at Datadog), covers:

1. Fundamentals of PBT
2. How to specify programs
3. Random generation
4. A practical implementation of PBT to test a key-value store using Hypothesis, in a hands-on sandbox.

Key concepts include:

• The software testing pyramid
• Qualities of a software test
• Differential testing
• Safety properties: idempotency, monotonicity, and round-trip properties
• Input generation

Throughout, we present various property blueprints for different domains, from frontend UI testing to backend systems and distributed applications.

The next installment will teach you how to apply property-based testing to entire distributed systems.

Transcript

Property-based testing and the test pyramid (00:00)

Hello everyone, welcome to “An Introduction to Property-Based Testing” by Antithesis. My name is Alp, I am a fifth-year PhD student working on property-based testing. We prepared this course with Antithesis for helping you raise the ceiling of what you can test and enhance the reliability of your systems. Even more so, to look at testing from a fresh, new perspective.

The course is divided into four chapters.

1. The first chapter discusses the vocabulary we use in describing software tests, different types of tests we run on our systems, how property-based testing fits in the landscape of testing, and why PBT is promising and useful.
2. In chapter two, we focus on properties, the method of specifying what it means to be correct in PBT. We talk about existing properties in systems we already have experience with, along with blueprints on how to apply them to new scenarios.
3. The focus of chapter three is random generation. Random generation is fundamental to the increased reliability we get from using PBT in our systems.
4. In chapter four, we will put our learnings into practice by property-based testing a key-value store. We will see how to write correctness properties for a key-value store, and we will also see how to write random generators for testing the properties we write.

The examples are going to be in Python, and we will use Hypothesis, a popular library in Python for writing property-based tests.

What you see on the right is the test pyramid, the largest source of our traditional understanding and vocabulary of software testing. The test pyramid mainly focuses on the scope of the tests. Going from unit to end-to-end tests, the cost of running the tests, the complexity of the tested behavior, and the time to run the tests themselves increases. And going down, the tests become more specific, verbose, and surgical. They measure much less, with higher precision. Despite its prominence, the test pyramid does not capture most of our understanding of what software tests are.

There are many test types in our daily workflows that cut through the test pyramid, because the test pyramid concerns itself with the scope, not the method or the purpose of testing. For instance, fuzz testing explores complex states in your applications by supplying random inputs to it. It tries to find paths in the program that could lead to crashes or assertion failures. Load and stress testing check system robustness under high traffic. Chaos testing checks system resilience under failures. Accessibility testing checks if an application is accessible to certain modes of usage.

Scope (02:50)

I will now present a framework that allows us to express such tests and talk about their qualities. We will talk about four different qualities of a software test, and the first is its scope. The scope of a test defines the input space that is in consideration. It is the answer to the question: “What do you test?” The simplest scope is a pure stateless function. The input space is the set of possible inputs to that function.

For a simple function like NEXT_DAY, where the input and output are days of the week, we would have seven possible inputs. For a function like power, there are going to be 264 possible inputs, because we are going to have two integers.

For a module or a class that defines an interface for interacting with it, the input space becomes the possible set of interactions we can take against the system. So you can imagine a queue, where we decide to either push or pop an item or peek at the top. These systems typically have some internal state too, which means we need to talk about the internal state when considering the possible sets of inputs in our testing process.

And as we start to discuss systems, we are becoming clients or consumers of those programs and we need to interact with the system from the outside. The input space is going to be a language. It could be a JSON schema for a REST API, SQL for SQLite, or C for GCC compiler. And it is going to be divided into two parts, well-formed and ill-formed inputs. At this point, valid errors for ill-formed inputs are going to become a concern on top of the previous behavior for well-formed inputs.

Purpose, specification, and method of proving inputs (04:38)

The second quality of a software test is its purpose. The purpose of a test is what it measures. Some tests measure functional correctness, the fact that the program returns the expected output for the given input. Some tests measure performance, the fact that the program finishes some given task under some time constraints. Some tests measure security of the program, the fact that the program does not leak secret data to public sources, or that it cannot be coerced into running unwanted code. Some tests measure resilience.

The third quality of a software test is its specification. Once we have a purpose, we need to know how to measure it. We need to specify a concrete measurement methodology. The simplest measurement is manual review. You run a piece of code, you personally overview the test, and you decide if the result of the execution conforms to your intent. You change the inputs, you view that the output changes as you expect it to, you tinker with the program. This is very typical in UI development, where it is hard to quantify the expectations. Hence programmers tend to rely on personal judgments and computer assisted tools.

Another example of specification is input-output specifications, the most popular of the codified specification mechanisms. In an I/O specification, you write multiple tests in the form of y = f(x), checking if running f(x) results in y. The I/O tests do not have to check for equality; they can also test other relations. For instance, we might write tests in the form of y in f(x), where f produces a list of items, and y is one of them.

We can also use IO tests for nonfunctional purposes. We can check that the time to execute f(x) with a smaller value is always shorter than the time to execute f(x) with a larger value, such as sorting short and long lists with similar characteristics. Or we can manually try known exploits and check that the result doesn’t leak some piece of data, such as SQL injections.

Sometimes, these I/O examples are going to be bespoke, but many times, they can be formulated as abstractions of a more general idea, which we will call properties. A property is a statement that we expect to be correct under any scenario. For instance, we can say that a linear traversal through a longer list will always take a longer time. We can formulate general statements such as “The absolute value of any number is at least zero,” or that “The program does not crash under any input,” or “There are never two leaders at the same time,” or “Running the program twice always leads to the same result,” and many, many more. We will focus much more on properties in the next chapter of the course.

The last quality that we will talk about is the method of providing inputs. The specification itself is not necessarily coupled with the method of providing inputs, at least for properties. You can test a property by manually constructing inputs yourself, systematically running through the possible set of inputs, randomly sampling the input space, or running symbolic methods or model checking for exhaustive checking. And you can combine these different methods too.

Throughout the course, I will focus on a specific testing paradigm, which we call property-based testing. Property-based testing couples properties as the method of specification with random generation as the method of supplying inputs. The examples we have will focus primarily on functions as their scope, and functional correctness as their purpose. Later modules will focus more on systems scope, specifically testing of distributed systems using deterministic simulation testing and fuzzing.

Benefits of property-based testing (08:57)

So, what’s so special and more so useful about property-based testing?

I like to think of PBT in software by thinking about all the other engineering artifacts I use in life. Imagine your car, and think about all the different conditions you use it: low speed in your neighborhood, high velocity on the highway, sometimes smooth, other times instant brakes, sunny on asphalt, snowy on gravel, rainy, icy, road with a pothole. Would you use a car that hasn’t been tested, tried, and investigated in a variety of different conditions?

Engineering defects are essentially out-of-distribution scenarios we forget to test our systems against, because if we had tested, we would have fixed it. In this context, software testing stands out as an outlier. Today’s mainstream approach to testing – I/O examples as specifications, where inputs are supplied by programmers manually – is essentially akin to testing the structural integrity of your building by jumping around your floor and flying paper planes from the side.

Properties allow us to capture complex, large-scale behaviors of our systems in abstract, as opposed to measuring small, concrete, singular behaviors of our systems. This property I will show you on the board captures what sorting is at a universal level, for all lists all at once very succinctly. The resulting list must be sorted, and it must have the same elements as the original one. We will not always have such nice properties; many systems we work with won’t have such succinct mathematical definitions. But as I will present to you throughout the module, there are many properties hidden right beneath our eyes.

As our systems get more complex, I/O examples become much more inadequate for defining correctness of a system. For instance, how would you even define the correctness of a function that flips a random coin using examples? How many examples does it take to define a correct C compiler? What about a database engine? The renderer in your browser? The navigation algorithm that takes you from your home to your office in the morning? Thousands? Hundreds of thousands? Maybe millions?

With properties, we acquire this superpower in simplicity. We do not need to define exactly what the compiler compiles to, but rather its relation. For instance, it must be the case that the programs produced by GCC and Clang must always have the same semantics. It is also the case that enabling compiler optimizations should not change the output of a program. We define these properties over all possible sets of programs, which is very empowering, but it also comes with the obligation of producing the inputs to test these properties, which will be in the generators chapter.

Differential testing (12:10)

Welcome to the second chapter of “Introduction to Property-Based Testing”: How to Specify Programs. In this chapter, we will learn how to specify programs through a series of popular properties in the wild, and their applications in front-end, back-end, and distributed systems.

Although many times the properties we work with will be domain-specific, there are templates, blueprints we can start from. We will go through these blueprints together; I will teach you how to apply those blueprints to your own work and to your own problems.

The first blueprint we will use is a differential test. Differential testing is all about equivalence. In order to prove that a scale is fair, we can put the same weight on both sides as much as we want, and measure that the scale is still balanced.

The compiler correctness property I have shown you is an instance of a differential test, where multiple implementations of the same standard behave identically. Another classic instance is a simple but correct reference implementation of a system against its complex, original, production-ready version. This might be a concurrent version of the same algorithm against a simple, single-threaded version of it, or a vectorized SIMD implementation against a good old for loop.

Let’s go over how we can construct such equivalence tests in UI programming. An important performance optimization in modern frontends is virtualization. A virtualized component renders only data visible to the user, rather than allocating DOM nodes for all of its elements, keeping the DOM small, reducing memory usage, and speeding up initial rendering, as well as scrolling. It is used for long lists, large tables, infinite scrolling feeds, and chat histories.

I have said that differential testing requires an equivalence, and virtualization has a natural equivalence to its nonvirtual or concrete counterpart. A virtualized list should have the same rendering and interactive behavior as its concrete version, which we are able to test.

A nice extension of differential testing is equivalence modulo x, meaning that the outputs are equal, except for some x factor that is supposed to change. And one instance is ensuring a change in a page component does not trigger a cascade of changes to the rest of the web page. It is contained in its own region.

So, what can you do? You can take the screenshot of a page, mark the area of the original component as dynamic, and the rest as static. Afterwards, you run the same inputs with both versions, and check that the static part is exactly the same.

We expect distributed systems to behave practically the same, regardless of the number of nodes. This gives us a natural definition of a differential property for many distributed systems. Please pause the video at this point and think of what such a property might be.

Welcome back, I hope you have had a good break. The answer to the question I posed is that we can differentially test the outputs of a multi-node system against a single-node version, expecting them to converge to the same outputs for the same inputs.

Safety properties and idempotency (15:47)

The second blueprint is not a property, but a class of properties that we will call safety properties. People have sensible expectations for any user-facing program. We expect that our file system is never corrupted, that we can always find the files where we had put them. We expect a video game to not crash between checkpoints, losing our progress. We hate it when an application gets stuck, leaving us with no choice but to restart it. We can express these properties as “x never happens” properties, and use random testing to try to find bugs – scenarios that push the program into these situations.

In terms of front-end or UI programming, we have: “The website responds to every local interaction in under 70ms.” This is a very decent property that I wish more websites had tested their systems on. “System does not crash” property can be tested in your UI too, making sure no sequence of interactions ever leads to a white page.

Another option is to check “system is never stuck,” meaning that there is always an interaction on the current page that the user can make progress with. For backend systems, there are many safety properties to be checked. Some of them are simpler to check: “Never crash the server,” “never experience data corruption.” Some of them are more domain-specific, requiring complex measurements or specifically-constructed scenarios, such as “always respond under three hundred milliseconds,” “narrowly leak users’ data to another user,” or “never double charge the customer.”

Idempotency is the property that doing something once is equivalent to doing the same thing many, many times. For instance, sorting is an idempotent function. Sorting once gives us the same result as sorting twice or three times. A good example of idempotency in practice is React’s useEffect. In strict mode, React runs each useEffect twice. Because useEffect must be idempotent, running it twice must not change the result. Idempotency is very crucial in a distributed systems context. As I’m sure Marco will spend a lot of time on it, I will not dive more into it in this module.

Whereas idempotency is about equivalence after many applications, monotonicity is about the editivity of results. A successive call to the same system with an existing result never decays, but only grows. There are lots of monotonic data in a growing system: IDs, counters, sizes. We can test the monotonicity of such data in the face of various complex interactions.

Roundtrip properties (18:37)

A roundtrip property is composed of two functions coupled with each other. Passing an input through f and then g yields the original input back. In other words, g is the inverse of f. Inverses are everywhere: decrement is the inverse of increment, pop is the inverse of append.

Roundtrip properties are particularly useful for parsing serialization. For parsers, the property is that you print an existing object you have, and then you parse the result of the printing operation back. For lossless compression, the property is that compressing some data and then decompressing the result of the compression should not result in loss of information. For serialization, the property is very similar to the parsers, where serializing and deserializing an object yields the original.

Let us take a moment to think why we want our serializers to conform to the roundtrip. For that, let’s imagine you and your best friend are sitting a bit apart in your least favorite class, and you need to gossip. You decide to pass them a message by writing your thoughts on a piece of paper. However, you cannot just pass them the paper, because your friend is not that close to you. So what do you do? You decide to make the paper into a ball. You throw the ball to them over the air, and they catch it. They uncurl the ball into the paper form, and read what you wrote.

This process has to conform to two nested roundtrip properties. The inner round trip is a compressed/decompressed round trip, meaning that you curling the ball into a ball and your friend uncurling the ball into a paper did not mess up the original message, remove any letters, or spill any ink on some other part of the message.

The other round trip is the print/parse round trip, meaning that your friend read the exact message you wrote, not mistaking “except” for “expect,” or “low” with “lose.” Maybe misunderstanding each other is fine for you and your friend, but it’s definitely not when millions of computers talk to each other every single second. So serializers and parsers of popular file formats, such as protocol buffer, Parquet, or Arrow, are extensively tested for round trips. I used to also give JSON.stringify() and JSON.parse() as an example of roundtrip too, but I learned that JSON_stringify() purposefully removes undefined values from objects, so roundtrip actually does not hold for this pair.

At the end of the day, correctness is inherently linked to your domain. Developing a chess engine will have vastly different notions of correctness than developing a database engine. Medical industries will have much stricter secrecy requirements than developer tools. Long-lived stateful programs will possess unknown states waiting to be discovered compared to one-off tools with minimal state. Many of the correctness properties in these systems will not fit into the categories that I have presented.

Many properties will have preconditions, predicates that define the conditions in which the property is valid for testing. For instance, a chess engine should assume that the opponent can never make an invalid move, and it should not be tested against such invalid movements. While testing a database, we can assume that the file will never be corrupted by another process. Or while testing a division routine, we can assume that the divisor will never be zero.

The different kinds of generators (22:31)

At the beginning of the course, I had told you about four different qualities of a software test, and how PBT fits into this categorization. In PBT, we use universal properties with random generation. So, once we have a universal property to be tested, we need the ability to generate random inputs for testing it. In this chapter, we will progressively generate more and more complex types, showing different ways of creating such generators.

So far, our discussions have been very abstract. We did not have much code, so we had not subscribed to any programming language. In this chapter, we will be using Python, and more specifically, a property-based testing library called Hypothesis. Hypothesis is a very mature PBT library with integrations to pytest, a large library of existing default generators for common data types, interfaces for creating new properties, and writing new random data generators from scratch.

Given a finite set, a generator is just a random pick over the set of elements. For a thirty-two-bit integer, we can just pick one of the two thirty-two elements in the set. For strings from an alphabet of k up to length n, the number of possible strings are: one for the empty string, k for strings of length one, k2 for strings of length two, and so on, of which we can pick any one of them.

For a small list that consists of four elements, we can define a set-based generator that will return each choice with a probability of 1/4. Composing generators for two different types is possible by making an initial random choice of picking one of the types, and then running its generator. It is akin to creating sets of sets, where we first select a set among the sets we have, and then select an element from the inner set that we had selected.

A recursive generator is similar to a recursive function, a generator that uses itself. Recursive generators are useful for generating recursive types such as JSON. As the generation needs to be bounded, there is typically a depth or size associated with each call to the generator. Each recursive call reduces the size, ensuring that the recursion terminates. In the JSON instance, we compose six different generators, two of which are recursive, the rest are just calls to the generators for the underlying types.

Composite generators are generators that compose the results of multiple generations for constructing complex objects. For instance, a generator for a list of type T first generates a random size n using a generator for natural numbers, and uses the generator for type T n times for producing a list of length n. We implement composite generators as sequences of generations, where the results of earlier generations can be passed as inputs to the later ones and affect the control flow of the generation process. This type of generation is in contrast to derived generation, which is purely syntactical.

Implementing the list generator (25:56)

Here is how to implement the list generator from scratch. For rather simple structures, it might be possible and also useful to write a generation that generates it purely from scratch. But there are lots of scenarios where this is not possible. Imagine you would like to test a SQL database. You need to generate random SQL statements to test against the database, but you also need random databases too.

It is not really possible to conjure a random database file by writing a generator for it. Hence, all projects in practice use random SQL statements for building up a random database, and then testing it with other random SQL statements and queries. As the state of the system under test is more complex, it is typical to start using the system’s own API for constructing its state before testing, instead of pure generation. Developing good generators takes time and intuition, as generators are hard to debug due to their non-deterministic nature.

So, I’ll give you some short tips. You must always measure your generators. When the generator is much more relaxed than the property expects, it will have lots of discards – inputs that are not tested because they were not valid inputs to begin with. Every discarded input is time and computation going to waste spending your testing budget in vain.

In the contrasting case, some generators are too narrow compared to the potential set of inputs. Imagine you only use SELECT queries for testing a SQL database. You are missing out on many, many interactions that might trigger bugs in your database. You can typically check coverage of your tests to see if you are missing large parts of the input space. Although having high coverage is not an indicator of good generators, low coverage can be an indicator of bad generators. Many PBT libraries allow for computing statistics for your testing campaigns. You can check your discard ratios, slice distribution, or any other statistics you would like to compute over your generated structures. A rather new tool, Tyche, will also be very useful. Tyche is a visualization tool with lots of good default statistics and analysis that you should be checking while running property-based tests, and it is also integrated with Hypothesis and Visual Studio Code.

Property-based testing a key-value store (28:31)

The first three chapters of the course have given quite a bit of conceptual information. We will now put them into practice by property-based testing a key-value store written in Python. The key-value store we work with is fairly basic. There is no concurrency support, which will be the main focus of the later modules. There is one central server, which holds all the data, and any number of clients can interact with the server, albeit serially.

There are four different message types.

The first message type is insert. insert takes two arguments: a key and a value. key is a string, and value is a JSON. If a value for the key already exists in the server, the server updates the value and returns the old value to the user.

The second message type is get. get takes one argument, a key. If a value for the key already exists in the key server, then the server returns the value, otherwise it returns none.

The third message type is delete. delete takes one argument, a key. If the value for the key exists in the server, the server removes the value and then returns it. Otherwise, it returns none.

The last message type is select. select takes one argument, a pattern. The pattern is fairly simple. It can have wildcards, which can match any number of unknown characters. The server returns the key-value pairs where the key fits the pattern.

In the rest of this chapter, we will start by discussing how we can test this system by going over what we need to generate, and how we can write said generators in Hypothesis. We will go over several properties at different levels, using existing blueprints we have talked about. As we have talked about in the generation chapter, generating complex structures from scratch isn’t always feasible. In such cases, we use the interface of the system to build up a state, instead of generating it from scratch. The specific system we work with, the key-value store, is not actually hard to generate from scratch for, because it is backed by a single Python dictionary. So, in theory, we could just generate random dictionaries that act as the storage unit of the key-value store, generate random inputs for messages, and test any property that we are interested in. However, although all key-value stores are dictionaries, not all dictionaries will be valid key-value stores, because the key-value store has special restrictions for the types of keys and values it possesses. We could overstep this problem by generating such restricted dictionaries, which I suggest you try as an exercise.

Instead, we went through the route of stateful generation. In order to generate a store, we first generate an empty store, then generate a number of random clients, and then generate a number of random messages by first picking a client, and then generating a random message from the client. Every interaction adds or removes data from the store, revealing more complex states of the store.

Properties in Python (32:10)

The first property we will talk about is the roundtrip property for message serialization. When a client sends a message to the server, they first create the message as an in-process Python object. This message is then serialized to a binary string, which is sent to the server over the network and is then deserialized in the server. If the server cannot deserialize the message, or worse, the server deserializes the message to a different message than the original one, the client cannot use the key-value store anymore. In order to avoid such failures, we want to test our serialization/deserialization logic. Without PBT, we would have used example-based tests where we assert the result of the serialization of a given message is a particular binary string. The roundtrip property gives us the opportunity to have a general notion of correctness, and random input generation allows us to test a very large number of scenarios under this test.

Let’s start by writing the property. The property uses a generator called messages, which we will see in a minute, that produces a random message that the predicate takes as its input. We start with an assume call, which says that empty strings should not be tested. This is a precondition of our property: we are saying that it only holds for non-empty keys, so Hypothesis will discard any input where the key of the message is an empty string.

The message is then serialized with the .serialize() code, and the result of the serialization is deserialized back in the next line. The assert in the last line is the crucial part that ties the knot, asserting that the original message should be the same as the deserialized one. As you can see, messages picks one of the potential message types and calls the generator for that message.

Next, we see inserts. We generate a random insert message. This is a composite generator in the terminology for Hypothesis, because it composes the results of different generators. Hypothesis uses the draw argument for enabling such compositions.

The generator first creates a key by generating a text, where the alphabet is printable strings, and the minimum size is zero, so empty strings are allowed, which will be discarded by the property as we had seen. The next step is to generate a random JSON value from scratch by using the JSON generator, and returning the constructed insert message at the end. You can check the generators for the other message types in the interactive playground.

Containment properties test the basic requirements of being a key-value store. We have two containment properties. The first is: inserted values should be in the store. The second is: deleted values should not be in the store.

Let’s start from the first one. We start from a random store state, a random set of clients, and a random insert message. We extract the key from the insert message to construct a get message that should get the inserted value. We first run the insert message against the store, and then run the get message that should successfully return the value that we had inserted. At the end, we assert that the returned value is equal to the inserted one.

We can test deletion similarly. We first run a wildcard select that should return all the values inserted by the clients we picked. We randomly select one of the key-value pairs and decide to delete it. We send a delete message to the server, which presumably removes the key-value pair from the store, and then we send a get message with the key we had just deleted. We assert that the result should be none.

What if we decide to switch the internal representation of our model from a dictionary to a more performant data structure, such as a prefix tree? The observable behavior should not change, right?

This should remind you of one of the blueprints we had talked about in the properties chapter, because we have two components that are equivalent to each other: differential testing. We can have two versions of our store: one backed by a dictionary and one backed by a prefix tree. Test both the correctness of the new prefix tree implementation compared to the original one, and also make sure our theoretical optimizations are actually realized in practice.