Counting Sheeps with Contracts in Python
I find code contracts fascinating, these are development tools that allows you to specify the behavior of your system, making it safer, easier to maintain, and a breeze to debug. They play well with your usual code-quality tools and are absolutely addicting once you start using them!
(traduction en français disponible)
I find code contracts fascinating, these are development tools that allows you to specify the behavior of your system, making it safer, easier to maintain, and a breeze to debug. They play well with your usual code-quality tools (continuous integration, unit tests, code reviews...), and they are are absolutely addicting once you start using them.
Through this post I will explain how they work, why they are so great, and how to use them in python through a small framework called dbc (that I'm the proud author of), I’ll also introduce some cool practices to follow when using them.
Let’s start from a fun example: counting sheeps. 🐑
We want to count the number of occurrences of the word sheep in a string, and once the 10th sheep is reached, the program will fall asleep.
In Python, it would be written something like
def count_sheeps(story : str) -> str:
"""
Counts sheeps, and fall asleep if 10 or more are provided.
Returns the text, up to the 10th sheep, with some snoring if the
10th sheep was reached.
"""
Running it on a text gives me… well it gives me at least part of the text back, with some snoring if the story is about sheeps, and no snoring in the other case. So it seems to work, but I can’t bother checking myself, for the text is quite long, and I wouldn’t want to risk falling asleep as well!
At this point, what I can do is to run some tests to make sure the implementation is correct, let’s do that, but the design-by-contract way!
What is design by contract (DbC)?
In order to test anything, you always need at some point to have test inputs assertions, and test assertions. The inputs will give you the context of the test, and the assertions will be the guide by which you will gauge the result. I guess it seems pretty basic and usual huh? Just hold my can of non-alcooholic beverage sourced from a fair agriculture and watch 🍺
In DbC, it’s the function itself that carries the assertion: the function is self-checking. Oh yes you know about that already, it's called doctest... NO it's not that at all.
In order to do carry the assertion, the technique requires “always true” things to check for, split between preconditions: things that are always true before the code executes and postconditions: things that are always true after the code executes.
When these conditions are indeed checked to be true, we say they hold, and execution continues without a hitch, otherwise we crash the program with a trace indicating which condition didn't hold that’s as simple as that. For those of you familiar with assertion, this is based on the same principles, but with some interesting twists!
Now in order to test, we also need inputs, DbC cannot really help you out of the box, but if you're interested in generating them you might have a look at fuzzing 🐇 For this simple example, we’ll just generate a nice story from chatGPT.
(Nota: you can also go as far as to mix contracts and fuzzing, for what is called semantic fuzzing, I’ll just leave the link there, because it’s a bit too on-the-edge for this post, but LMK if you're interested in knowing more!).
Adding the conditions
Let’s now try to find some pre- and post-conditions for the code to work with.
First of all, I expect some string to be provided otherwise my code will crash. That gives us a first condition, one that must be true right before the code is executed, in other words: a precondition
isinstance(story, str)
Then, if I assume the resulting string is in the variable result, I need it to be a string once execution is finished. This is a postcondition.
isinstance(result, str)
That’s not all, I know some information about what I want as a result: It needs to contain the text given, stopped right before the 10th sheep, that is:
- If there are less than 10 occurrences of sheep in the result
story.count("sheep") < 10
- then we return the full story without falling asleep (like a big boy we are)
result == story
- else - and it’s a bit more involved - the result must be the initial string up to the 10th sheep, and then a single snore
result.count("sheep") == 9
result == story[: len(result) - len(snoring)]) + snoring
- then we return the full story without falling asleep (like a big boy we are)
Now in terms of putting it all together down as pre- and post-condition, let’s make use of the dbc framework.
@precondition(lambda story: isinstance(story, str))
@postcondition(lambda story, result: result.count("sheep") < 10)
@postcondition(
lambda story, snoring, result: result == story
if story.count("sheep") < 10
else result.count("sheep") == 9 and result == story[: len(result) - len(snoring)]) + snoring
)
def count_sheeps(story: str, snoring: str = "\nZzzz...") -> str:
Aside: syntax help
The framework declares the @precondition and @postcondition decorators. which are a nice way of adding some code around an existing function without modifying its implementation directly, and expressed the conditions to check using lambda expressions.
That’s probably a bit too much to take in if you’re not familiar with Python’s functional / expression syntax or with JavaScript's anonymous functions, so let’s just take the time to unpack a bit of the syntax:
@precondition(lambda story: isinstance(story, str))
I’m using the @precondition, with the @ marking it as a decorator. That means that the parameter in parentheses is the precondition function. This function lambda story: isinstance(story, str)
is written as a lambda expression: an anonymous (it has no proper name) function, which takes as parameters what’s before the colon :
,that would be story
, and returns what comes after, that is isinstance(story, str)
.
So we are checking for the first condition we laid down: story is an instance of str.
The way it will work is that whenever we call count_sheeps
, the dbc framework will first call this lambda expression with the actual value of the story parameter, and it will act accordingly: story
is a str
? Ok, it's as expected, nothing to see there 👮🏻, the call can happen. If not, it's a bug, the framework will now do its thing.
You can also notice that there is a result
parameter that might pop-in in the post-condition, this parameter is the value that the function return
’d, that’s as simple as that.
There’s also an old
parameter, which I didn’t use there, it contains the value of the parameters before the function call, that is pretty interesting for a functions that should mutate an object (e.g. adding an element to the parameter list_of_things
so that we'll want to check the value of the list at time of output with that at time of input).
Back to DbC
What happens if the conditions are not respected, you might ask.
At each time that the function is called, there are 3 steps:
- The pre-condition is checked. Since it checks the arguments before the call happens, it means that a failing pre-condition must mean the caller function is at fault.
- The call is performed, the function takes correct inputs, and it calculates a result
- The post-condition is checked - and here comes the kicker: since the pre-condition holds, the post-condition must hold as well, otherwise it means that the implementation is at fault.
Let’s put that into action
count_sheeps(10) # oh no, it’s not a string!
AssertionError: **caller** of count_sheeps() bug: precondition 'isinstance(story, str)' failed: story = 10
def count_sheeps(story: str, snoring: str = "\nZzzz...") -> str:
return snoring # early sleeper, heh
AssertionError: count_sheeps() bug: postcondition 'result == story' failed: result = '\nZzzz...', snoring = '\nZzzz...', story = '\nIn a quiet [...]p.\n\nTHE END'
You see that in both cases, the framework does several things to help you debug the code:
- Identify where the bug comes from: the calling context, or the function's implementation
- Displaying the exact condition that failed
- Displaying the inputs provided, so that you can debug the failing cause yourself
- NB: This in itself constitutes a valid piece of test data for integration into unit testing!
Now if you want to know about, trace, and debug all the crashes of your app, what's greater and simpler to use than this kind of framework, you tell me ?!
High-level overview
Let's take a step back and just review what I've discussed there, from a higher standpoint.
Contracts can be seen as executable, living, piece of documentation, if you look at their use above, you can see that there’s few things that a comment could add in terms of how to use this subprogram, but it can then focus on the why (ding ding ding 🔔 good software practices!).
Also you can notice that I didn’t put the implementation in, in fact you don’t need it at all to understand what is being done: the implementation is the how. For all we know it sends the story to someone that reads it out loud to a small child (or an older child, try a 30+ year old young parent, that should work as well) and notify us when the child is sound asleep.
Implementation doesn’t matter, which makes that a perfect tool for math-oriented people, as the joke goes: a mathematician sees a burning trash in the street, they go “ah, not interesting, I know how to solve that” and go along with their day without extinguishing the fire.
Finally, contracts lend themselves naturally to work at scale, in the form of what we call percolating, and that's the actual real game-changer aspect of this practice.
Percolating conditional is when you have contracts around a function you call, for example if you have a calling code call_count_sheep
for count_sheep
, what should the contracts of this function be? Well, depends on what it does, but if in any case it calls count_sheep
, you can already identify some: these are the same as count_sheep
! Copy-pasting them will simply work. Or refactoring them if you don't want to copy paste all around. This is, after all, just code!
@precondition is the same as count_sheep!
@postcondition is the same as count_sheep!
def call_count_sheep(story : str) -> str:
... # unrelated work
return count_sheep(story)
Conclusion
To lay down some additional advantages to this way of using DbC
- this is code that you can execute, so the user can actually check the pre-condition before causing an error to be raised (and that’s actually a good practice!)
- syntax is that of pure Python, so any users will be able to understand it “out of the box” (no weird custom syntax to learn - looking at you doctest 👀)
- it is “always” up-to-date, because it “always” checked (actually, for performance reasons you will want to disable most of them in production, but that’s a story for a different time 😜)
- unit tests just write themselves (if that’s not clear why, fret not, I’ll get into more details in another post)
That’s it, that’s all that this does, but this might already feel a little bit magical if you’re unused to the arcane art of python functional coding and reflection, but thankfully this is all nicely wrapped within the dbc framework, and that’s all you have to care about.
In a next blog post, I’ll explain how I implemented these by using some python dark magic, and how DbC can be used in parallel to your usual dev techniques to unlock tons of productivity gains during coding and unit testing. I also want to talk about easing into unit-test thanks to it, and how to use that on huge complicated badly documented API (looking at you python-gitlab and google cloud API 👀) to help in discovering and documenting them internally. Let me know if any of this scratches an itch 😉
This is my first real blog post, so I’m very interested in your opinion, and I’ll happily oblige by answering any question or comment you can have, so don’t hesitate to put them below or send them to me directly (contact at the bottom).
Happy code-painting!
Some links for reference
DbC Framework used in the examples
Software concepts
Python concepts
Other ressources
Semantic fuzzing with zest [ISSTA 2019] on the ACM website