Types and Specifications

Previous in the series: https://medium.com/@robert_70579/playing-the-wrong-game-32745fa3bac7

https://commons.wikimedia.org/wiki/File:Krzywy_Las_-_Nowe_Czarnowo_2.JPG

Just because you’ve counted all the trees doesn’t mean you’ve seen the forest. — Anonymous

In my previous post about testing I made the case for setting a different metric for how testing can be used to create high quality code. Using the goal of high coverage is not a sufficient metric to drive good software but what is? Fortunately coverage is not the only tool in our toolbox.

One of the first tools used by languages to put guarantees on the behavior of programs was the type system. With it, invalid operations can be caught at compile time and in more in sophisticated languages polymorphic types can describe the behavior of objects and operations while letting implementation details be determined separately. Types write a contract between the objects and functions of a program that can be enforced by the system leaving the developer to think about other concerns. The way this is done in most languages, though, can create confusion and boiler plate code (I’m looking at you Java abstract classes). Type systems solve some problems while generating new ones and although the net effect is positive they still leave something to be desired.

While a type system, especially one that allows polymorphic interfaces, is a powerful tool it isn’t quite enough to guarantee correctness. Some languages have chosen to discard the type system but others have created a new beast that has many of the advantages of types and unlocks a powerful new set of tools. While this transformation has occurred in many languages I will illustrate in Clojure.

Let’s start with a simple function to take any string formatted day from perhaps a JSON payload and returns if it is my birthday.

Seems reasonable right? Two valid inputs that showed the code produces the expected results. Not really, though, the function is taking an arbitrary function argument and making several assumptions about it.

That exception was not covered by the original tests despite what a coverage tool may say. If it made it to production it could cause an unhandled exception to crash software and perhaps tie the developer up in knots finding it. One approach to this in Clojure is spec. It allows a programmer to make assertions about bindings such as input arguments. The first step is to use it like a type assertion in a strongly typed language:

This is closer. This example models exception handling code with an extra special exception that is a stand in for dealing with invalid input types. This is good but what about when the function gets an input like this:

Well that was unhelpful. The input was a string like the type system asserted but it wasn’t a good enough string. Fortunately spec doesn’t just limit code to type assertions (already a huge step forward). These specs can be arbitrary functions that programmatically describe the requirements of that argument. This doesn’t work like an abstract class that asserts the presence of methods but instead allows the function to specify properties directly.

This gets the function there. No only does it type assert that the input is a string but it defines abstract properties of the content (the nature?) of that string. Still, you can imagine that these tests are not sufficient. What if I could somehow create a huge list of dates and run them all through my function? Maybe I could compile a blessed dataset with thousands, maybe millions of date strings. Different centuries, different formats? I could set up a batch job to run on every build and verify that my function never failed. In this example that is clearly overkill but software engineers are solving these sorts of problems in this way. We need something better and the academics came up with it.

In Haskell it was called QuickCheck and it sought to describe the behavior of a function in such a way that a program could perform the search for bugs for you. I encourage you not to take my word for it and look up John Hughes many videos on the subject (not the Hollywood director, be sure to add QuickCheck to those searches). Several languages have implemented the methods of QuickCheck or now it is generally referred to as “generative testing” including in Clojure. This is documented here: https://clojure.org/guides/spec#_generators, but this example makes us take things a bit farther.

First of all what does the “string?” spec generated data look like:

While those are certainly strings I wonder if a string generator will ever generate an RFC3339 string for my birthday? How many iterations would it take? ~2¹⁶⁰ in ASCII could take a while. I don’t have that kind of time. What about the perfectly functional spec used above:

Yup, there is no free lunch. It is easy to create a function that describes what doesn’t work but creating a function that limits my options is more difficult. Fortunately gen has several building blocks such as ranges of numbers and dates. It also includes the ability to transform and combine these building blocks. This is illustrated with the following generator:

This will generate string representations of dates between 1900 and 2100.

Checks out. The last step is to describe the behavior of the function itself in a similar way.

As a sceptic, I don’t immediately believe that this generator will guess the 200 occurrences of my birthday in such a wide range so I intentionally specified the function behavior incorrectly.

More than half the time the above represents the result. With some confidence that at least it should find a failure I’ll construct a more realistic function spec:

Now, granted this example is pretty simple and I’ve simply implemented the function spec as an alternative method but it serves to give an example of how a complex interaction (such as communicating with another system) can be described by simpler functions for the sake of a generator.

Success! The science behind generative tests is something I encourage everyone who cares about quality software spends time looking into. Hughes has made a career instructing developers in these methods and doing contract work where his team finds esoteric and seemingly illogical bugs in the software that keeps us safe and runs the modern world. By taking this approach, or even simply taking the step toward descriptive function behavior with spec it is possible to remove the repetition and guess work from writing tests and even mathematically prove correctness.

Code examples can be found here:

spec_vs_type.clj

and are covered by MIT license if you are interested.

Next in the series: https://itnext.io/quickcheck-testing-in-golang-772e820f0bd5