Introduction to Properties-driven Development

Properties-driven development

There are plenty of tools available to help here, and for software developers, test-driven development (TDD) is one of the most frequently used approaches. TDD forces us to position ourselves first as a user of the program rather than an implementer. Before writing any new feature, we first need to write a failing test exercising the feature and then write the code to make it pass. All program improvements are a series of small iterations built on well-understood foundations.

This kind of approach can be interesting in the context of property-based testing. Before writing a program, we’ll want to think about what it should do. Unsurprisingly, we’ll want to encode these assumptions as rules for properties. Then, we’ll run our program against them as we go. What happens next is a series of increasing failures, where we have to figure out if it’s the program that is wrong or our understanding of what it should do in the first place that needs to change.

In this chapter, we’ll go through a properties-driven approach and explore techniques related to positive tests (validate what the program does) and negative ones (test what the program can’t handle). We’ll also push generators further than we’ve done before, which will be a good exercise on its own. We’ll do all of that by developing a short program inspired by the Back to the Checkout code kata, where we implement a pricing system for a supermarket.

The specification

Although it’d be great to have a well-defined specification, we’ll work from a more realistic starting point by keeping things vague. We’ll write a system that’s given a bunch of items that have been scanned. We have to look up the price of these items and calculate the total amount to charge. We can also play with instant rebates for certain items. For instance, certain items could be priced at two for the price of one (2 shirts for the price of 1), or a specific amount for a specific price (5 bags of chips for $7).

In fact, the code kata gives the following table:

Item	Unit Price	Special Price
A	50	3 for 130
B	30	2 for 45
C	20
D	15

The checkout function should accept items in any order, so ["B", "A", "B"] would give the 2-for-45 rebate for the B items being bought. The only call that needs to be exposed is checkout:total(ListOfItemsBought, UnitPrices, SpecialPrices) → Price.

That’s it. The requirements are vague, but we can extract the following list of things to tackle:

• Items are identified by unique names, meaning non-empty strings.
• The list of items has no set length, and the items it contains are in no specific order.
• The unit prices appear to be integers.
• The special prices are triggered only once the right number of items of the proper type can match a given special.
• All items have a unit price.
• It is not mandatory for a given item to have a special price.

The rest is seemingly undefined or underspecified, so the assumptions we bake into the program about the rest could be tricky and bug-prone.

Aside from these requirements, here are two possible properties:

1. Without any special prices defined, the total is just the sum of all of the items’ prices.
2. With a known count for each item, the total comes from two parts added together. These two parts are the special price multiplied by the number of times it can be applied to a given set of items and the remainder which is added on top of the special prices.

Since we’re interested in discovering and improving the design of the program through properties, we can start by implementing the first two properties we’ve come up with, and then writing the code to make them pass. This will bring us to a point where the basic program does what we want. Then, we’ll see how properties can be used in negative tests, checking that the program does what we want, but also deals with things we don’t want to happen.

So, let’s get started with writing our first property.