Types + Properties = Software: state transition properties by Mark Seemann
Specify valid state transitions as properties.
This article is the second in a series of articles that demonstrate how to develop software using types and properties. In the previous article, you saw how to design with types so that illegal states are unrepresentable. In this article, you'll see an example of how to express properties for transitions between legal states.
The source code for this article series is available on GitHub.
This article continues the Tennis Kata example from the previous article. It uses FsCheck to generate test values, and xUnit.net as the overall test framework. It also uses Unquote for assertions.
State transitions #
While the types defined in the previous article make illegal states unrepresentable, they don't enforce any rules about how to transition from one state into another. There's yet no definition of what a state transition is, in the tennis domain. Let's make a definition, then.
A state transition should be a function that takes a current Score and the winner of a ball and returns a new Score. More formally, it should have the type Score -> Player -> Score.
(If you're thinking that all this terminology sounds like we're developing a finite state machine, you're bang on; that's exactly the case.)
For a simple domain like tennis, it'd be possible to define properties directly for such a function, but I often prefer to define a smaller function for each case, and test the properties of each of these functions. When you have all these small functions, you can easily combine them into the desired state transition function. This is the strategy you'll see in use here.
Deuce property #
The tennis types defined in the previous article guarantee that when you ask FsCheck to generate values, you will get only legal values. This makes it easy to express properties for transitions. Let's write the property first, and let's start with the simplest state transition: the transition out of deuce.
[<Property>] let ``Given deuce when player wins then score is correct`` (winner : Player) = let actual : Score = scoreWhenDeuce winner let expected = Advantage winner expected =! actual
This test exercises a transition function called scoreWhenDeuce. The case of deuce is special, because there's no further data associated with the state; when the score is deuce, it's deuce. This means that when calling scoreWhenDeuce, you don't have to supply the current state of the game; it's implied by the function itself.
You do need, however, to pass a Player argument in order to state which player won the ball. Instead of coming up with some hard-coded examples, the test simply requests Player values from FsCheck (by requiring the winner function argument).
Because the Player type makes illegal states unrepresentable, you're guaranteed that only valid Player values will be passed as the winner argument.
(In this particular example, Player can only be the values PlayerOne and PlayerTwo. FsCheck will, because of its default settings, run the property function 100 times, which means that it will generate 100 Player values. With an even distribution, that means that it will generate approximately 50 PlayerOne values, and 50 PlayerTwo values. Wouldn't it be easier, and faster, to use a [<Theory>] that deterministically generates only those two values, without duplication? Yes, in this case it would; This sometimes happens, and it's okay. In this example, though, I'm going to keep using FsCheck, because I think this entire example is a good stand-in for a more complex business problem.)
Regardless of the value of the winner argument, the property should hold that the return value of the scoreWhenDeuce function is that the winner now has the advantage.
The =! operator is a custom operator defined by Unquote. You can read it as a must equal operator: expected must equal actual.
Red phase #
When you apply Test-Driven Development, you should follow the Red/Green/Refactor cycle. In this example, we're doing just that, but at the moment the code doesn't even compile, because there's no scoreWhenDeuce function.
In the Red phase, it's important to observe that the test fails as expected before moving on to the Green phase. In order to make that happen, you can create this temporary implementation of the function:
let scoreWhenDeuce winner = Deuce
With this definition, the code compiles, and when you run the test, you get this test failure:
Test 'Ploeh.Katas.TennisProperties.Given deuce when player wins then score is correct' failed: FsCheck.Xunit.PropertyFailedException : Falsifiable, after 1 test (0 shrinks) (StdGen (427100699,296115298)): Original: PlayerOne ---- Swensen.Unquote.AssertionFailedException : Test failed: Advantage PlayerOne = Deuce false
This test failure is the expected failure, so you should now feel confident that the property is correctly expressed.
Green phase #
With the Red phase properly completed, it's time to move on to the Green phase: make the test(s) pass. For deuce, this is trivial:
let scoreWhenDeuce winner = Advantage winner
This passes 'all' tests:
Output from Ploeh.Katas.TennisProperties.Given deuce when player wins then score is correct: Ok, passed 100 tests.
The property holds.
Refactor #
When you follow the Red/Green/Refactor cycle, you should now refactor the implementation, but there's little to do at this point
You could, in fact, perform an eta reduction:
let scoreWhenDeuce = Advantage
This would be idiomatic in Haskell, but not quite so much in F#. In my experience, many people find the point-free style less readable, so I'm not going to pursue this type of refactoring for the rest of this article series.
To be continued... #
In this article, you've seen how to express the single property that when the score is deuce, the winner of the next ball will have the advantage. Because illegal states are unrepresentable, you can declaratively state the type of value(s) the property requires, and FsCheck will have no choice but to give you valid values.
In the next article, you'll see how to express properties for slightly more complex state transitions. In this article, I took care to spell out each step in the process, but in the next article, I promise to increase the pace.
If you're interested in learning more about Property-Based Testing, you can watch my introduction to Property-based Testing with F# Pluralsight course.
