TDD makes you think hard about your code, property-based TDD makes you think even harder.
I'll try to do this exercise myself, though I take an easier way: with Haskell.
First Keith's rule is: Write exactly one new test, the smallest test you can that seems to point in the direction of a solution. And this is hard. Nat took quite a big step, thinking already about a winner in a beginning. We don't get even close, in this quite lengthy post.
Returning back to the Tic-Tac-Toe: What are the types of data and operation we can start from? We write our types first.
That feels like a lot of types already, but I can't state any interesting properties about moves, without tying them to the game (giving them order).
Than the operation simplest operation (actually I cheat here, I have already sub-goal in my mind: I want eventually define isValidMove :: Game -> Move -> Bool predicate).
Then what will be our first property? maybe: forall g :: Game, exists p :: Position, isFreePosition g p. This one isn't true for all games. Counter-example is the game with 9 moves. We refine our property to: forall g :: Game, length . unGame g < 9, exists p :: Position, isFreePosition g p. This property is problematic as well. First of all, it's existential. We can turn it around into: forall g :: Game, length . unGame g == 9, forall p :: Position, isFreePosition g p = False.
This property we can QuickCheck:
As expected QuickCheck found undefined after one test (as isFreePosition is always undefined for now).
Now we try to turn red into green, let's implement isFreePosition properly.
You can argue this implementation isn't proper, but all tests are green!
New tests, red again
So we need more tests (properties), every position is free in just started game: forall p :: Position, isFreePosition (Game ) p.
Turning green II
Again red. Let's fix isFreePosition:
What's wrong? We can implement shrink for Game9, which hopefully will make counterexample more descriptive:
It's easy to see that all moves in the game are same! But that doesn't make sense! And that's our fault.
Turning green, try III.
Our game9_no_free_positions_prop property is bogus. We could restate it into something more precise: forall g :: Game, length . ungame g >= 9, isValidGame g, forall p :: Position, isFreePosition g p = False, where isValidGame is something like:
But we are red, so we don't touch properties.
isValidGame is an Game invariant we want to hold always. If we hide Game implementation details, and expose only invariant preserving operations, forall g :: Game, isValidGame g will be true (and we can state this property!). Unfortunately we have to change our tests a little bit, as we give things name, like moveCount = length . unGame. That we could do right from beginning.
I use assert in addMove functions. Why?
Because I cannot state the pre-condition in types. The situation is similar to division by zero.
Looks pretty good already, except there are unused unPosition and movePlayer function. I thought to much up front, we could get here without Player type at all. However natural next step would be to write code that will eventually use movePlayer. Like defining isNextPlayer :: Game -> Player -> Bool predicate and going thru similar steps we already went thru with isFreePosition. I leave that as an exercise for a reader.
At some point, I got insight, that properties aren't specific to Tic-Tac-Toe game. The only Tic-Tac-Toe specific part is magic constant9. It is 64 for Reversi, 361 for 19×19 board of Go or Gomoku. So we came up with some general board game properties!