Difficulty thinking of properties for FsCheck

Question

I've managed to get xUnit working on my little sample assembly. Now I want to see if I can grok FsCheck too. My problem is that I'm stumped when it comes to defining test properties for my functions.

Maybe I've just not got a good sample set of functions, but what would be good test properties for these functions, for example?

//transforms [1;2;3;4] into [(1,2);(3,4)]
pairs : 'a list -> ('a * 'a) list      //'

//splits list into list of lists when predicate returns 
//  true for adjacent elements
splitOn : ('a -> 'a -> bool) -> 'a list -> 'a list list

//returns true if snd is bigger
sndBigger : ('a * 'a) -> bool (requires comparison)

Morna

Answer 1

There are already plenty of specific answers, so I'll try to give some general answers which might give you some ideas.

1. Inductive properties for recursive functions. For simple functions, this amounts probably to re-implementing the recursion. However, keep it simple: while the actual implementation more often than not evolves (e.g. it becomes tail-recursive, you add memoization,...) keep the property straightforward. The ==> property combinator usually comes in handy here. Your pairs function might make a good example.
2. Properties that hold over several functions in a module or type. This is usually the case when checking abstract data types. For example: adding an element to an array means that the array contains that element. This checks the consistency of Array.add and Array.contains.
3. Round trips: this is good for conversions (e.g. parsing, serialization) - generate an arbitrary representation, serialize it, deserialize it, check that it equals the original. You may be able to do this with splitOn and concat.
4. General properties as sanity checks. Look for generally known properties that may hold - things like commutativity, associativity, idempotence (applying something twice does not change the result), reflexivity, etc. The idea here is more to exercise the function a bit - see if it does anything really weird.

As a general piece of advice, try not to make too big a deal out of it. For sndBigger, a good property would be:

let ``should return true if and only if snd is bigger`` (a:int) (b:int) = sndBigger (a,b) = b > a

And that is probably exactly the implementation. Don't worry about it - sometimes a simple, old fashioned unit test is just what you need. No guilt necessary! :)

Maybe this link (by the Pex team) also gives some ideas.

Belton

The given link is dead. The corrected link may be research.microsoft.com/en-us/projects/pex/patterns.pdf – Laidlaw

Note that all those things we were taught in grade school math ((commutative property, associative property, distributive property...) that were quite useless unless you went to graduate school in Mathematics), are the most obvious candidates for properties-based testing. High school geometry and its theorems provide additional inspirations for property tests. Try to channel this kind of thinking when devising property tests. If you sum non-negative numbers, the result will be non-negative. Look for such insights into your codebase. – Mercer

Answer 2

I'll start with sndBigger - it is a very simple function, but you can write some properties that should hold about it. For example, what happens when you reverse the values in the tuple:

// Reversing values of the tuple negates the result
let swap (a, b) = (b, a)
let prop_sndBiggerSwap x = 
  sndBigger x = not (sndBigger (swap x))

// If two elements of the tuple are same, it should give 'false'
let prop_sndBiggerEq a = 
  sndBigger (a, a) = false

EDIT: This rule prop_sndBiggerSwap doesn't always hold (see comment by kvb). However the following should be correct:

// Reversing values of the tuple negates the result
let prop_sndBiggerSwap a b = 
  if a <> b then 
    let x = (a, b)
    sndBigger x = not (sndBigger (swap x))

Regarding the pairs function, kvb already posted some good ideas. In addition, you could check that turning the transformed list back into a list of elements returns the original list (you'll need to handle the case when the input list is odd - depending on what the pairs function should do in this case):

let prop_pairsEq (x:_ list) = 
  if (x.Length%2 = 0) then
    x |> pairs |> List.collect (fun (a, b) -> [a; b]) = x
  else true

For splitOn, we can test similar thing - if you concatenate all the returned lists, it should give the original list (this doesn't verify the splitting behavior, but it is a good thing to start with - it at least guarantees that no elements will be lost).

let prop_splitOnEq f x = 
  x |> splitOn f |> List.concat = x

I'm not sure if FsCheck can handle this though (!) because the property takes a function as an argument (so it would need to generate "random functions"). If this doesn't work, you'll need to provide a couple of more specific properties with some handwritten function f. Next, implementing the check that f returns true for all adjacent pairs in the splitted lists (as kvb suggests) isn't actually that difficult:

let prop_splitOnAdjacentTrue f x = 
  x |> splitOn f 
    |> List.forall (fun l -> 
         l |> Seq.pairwise 
           |> Seq.forall (fun (a, b) -> f a b))

Probably the only last thing that you could check is that f returns false when you give it the last element from one list and the first element from the next list. The following isn't fully complete, but it shows the way to go:

let prop_splitOnOtherFalse f x = 
  x |> splitOn f
    |> Seq.pairwise 
    |> Seq.forall (fun (a, b) -> lastElement a = firstElement b)

The last sample also shows that you should check whether the splitOn function can return an empty list as part of the returned list of results (because in that case, you couldn't find first/last element).

Lotz

Thanks, I'll have to try some of these ideas. – Morna

Great, thorough answer. However, your prop_sndBiggerSwap doesn't always hold, since sndBigger (z,z) = sndBigger (swap (z,z)) for all z. – Appleby

@kvb: Thanks - you're of course right! I editted the post to show a corrected version of the rule. – Lotz

That's a great answer Tomas. A few remarks: it's better to keep the properties non-polymorphic, this is usually accomplished by given a appropriate type annotation e.g. let prop_pairsEq (x:int list) =. Furthermore, FsCheck can generate arbitrary functions (with some small print, see the documentation on coabitrary). They will be pure. – Belton

@Kurt: Very useful practical tips, thanks! Honestly, I don't have much practical experience with FsCheck - my answer was based on the algebraic laws that I would expect to hold (monad laws and arrow laws are a good way to practice this kind of thinking) – Lotz

Answer 3

For some code (e.g. sndBigger), the implementation is so simple that any property will be at least as complex as the original code, so testing via FsCheck may not make sense. However, for the other two functions here are some things that you could check:

• pairs
  • What's expected when the original length is not divisible by two? You could check for throwing an exception if that's the correct behavior.
  • List.map fst (pairs x) = evenEntries x and List.map snd (pairs x) = oddEntries x for simple functions evenEntries and oddEntries which you can write.
• splitOn
  • If I understand your description of how the function is supposed to work, then you could check conditions like "For every list in the result of splitOn f l, no two consecutive entries satisfy f" and "Taking lists (l1,l2) from splitOn f l pairwise, f (last l1) (first l2) holds". Unfortunately, the logic here will probably be comparable in complexity to the implementation itself.

Appleby

Thanks for the tips. I'm already checking for the exception with xUnit, so no added value there (as far as I can tell?). It all seems very thinky-out-the-boxy for me at the moment, and as you say, in these specific cases, the tests risk being more complicated than the originals. – Morna

The checks should not be more complicated - that indeed defeats the purpose of testing. but they can be equally complex, in my experience. With time, your implementation may become more complex (e.g. optimizations), while the properties/specifications usually remain more or less the same. So while it might not make sense now, you'll probably be happy with the properties later. – Belton