What to use property testing for

Question

I'd like to know what is the property testing aiming for, what is it's sweet point, where it should be used. Let' have an example function that I want to test:

f :: [Integer] -> [Integer]

This function, f, takes a list of numbers and will square the odd numbers and filter out the even numbers. I can state some properties about the function, like

1. Given a list of even numbers, return empty list.
2. Given a list of odd numbers, the result list will have the same size as input.
3. Given that I have a list of even numbers and a list of odd numbers, when I join them, shuffle and pass to the function, the length of the result will be the length of the list of odd numbers.
4. Given I provide a list of positive odd numbers, then each element in the result list at the same index will be greater than in the original list
5. Given I provide a list of odd numbers and even numbers, join and shuffle them, then I will get a list, where each number is odd
6. etc.

None of the properties test, that the function works for the simplest case, e.g. I can make a simple case, that will pass these properties if I implement the f incorrectly:

f = fmap (+2) . filter odd

So, If I want to cover some simple case, It looks like I either need to repeat a fundamental part of the algorithm in the property specification, or I need to use value based testing. The first option, that I have, to repeat the algorithm may be useful, If I plan to improve the algorithm if I plan to change it's implementation, for speed for example. In this way, I have a referential implementation, that I can use to test again.

If I want to check, that the algorithm doesn't fail for some trivial cases and I don't want to repeat the algorithm in the specification, it looks like I need some unit testing. I would write for example these checks:

f ([2,5]) == [25]
f (-8,-3,11,1) == [9,121,1]

Now I have a lot more confidence it the algorithm.

My question is, is the property based testing meant to replace the unit testing, or is it complementary? Is there some general idea, how to write the properties, so they are useful or it just totally depends on the understanding of the logic of the function? I mean, can one tell that writing the properties in some way is especially beneficial?

Also, should one strive to make the properties test every part of the algorithm? I could put the squaring out of the algorithm, and then test it elsewhere, let the properties test just the filtering part, which it looks like, that it covers it well.

f :: (Integer -> Integer) -> [Integer] -> [Integer]
f g = fmap g . filter odd

And then I can pass just Prelude.id and test the g elsewhere using unit testing.

Answer 1

How about the following properties:

1. For all odd numbers in the source list, its square is element of the result list.
2. For all numbers in the result list, there is a number in the source list whose square it is.

By the way, odd is easier to read than \x -> x % 2 == 1