Equational laws for free
Haskell C
Latest commit 21015d2 Mar 16, 2017 @nick8325 committed on GitHub Merge pull request #20 from NorfairKing/redundant-monoid-import
Added cpp for a redundant monoid import


QuickSpec: equational laws for free!

Ever get that nagging feeling that your code must satisfy some algebraic properties, but not sure what they are? Want to write some QuickCheck properties, but not sure where to start? QuickSpec might be for you! Give it your program — QuickSpec will find the laws it obeys.

QuickSpec takes any hodgepodge of functions, and tests those functions to work out the relationship between them. It then spits out what it discovered as a list of equations.

Give QuickSpec reverse, ++ and [], for example, and it will find six laws:

xs++[] == xs
[]++xs == xs
(xs++ys)++zs == xs++(ys++zs)
reverse [] == []
reverse (reverse xs) == xs
reverse xs++reverse ys == reverse (ys++xs)

All the laws you would expect to hold, and nothing more — and all discovered automatically! Brill!

Where’s the catch? While QuickSpec is pretty nifty, it isn’t magic, and has a number of limitations:

  • QuickSpec can only discover equations, not other kinds of laws. Luckily, equations cover a lot of what you would normally want to say about Haskell programs. Often, even if a law you want isn’t equational, QuickSpec will discover equational special cases of that law which suggest the general case.

  • You have to tell QuickSpec exactly which functions and constants it should consider when generating laws. In the example above, we gave reverse, ++ and [], and those are the only functions that appear in the six equations. For example, we don’t get the equation (x:xs)++ys == x:(xs++ys), because we didn’t include : in the functions we gave to QuickSpec. A large part of using QuickSpec effectively is choosing which functions to consider in laws.

  • QuickSpec exhaustively enumerates terms, so it will only discover equations about small(ish) terms. You can adjust the maximum terms but, as QuickSpec exhaustively enumerates terms, there is an exponential blowup as you increase the depth. Likewise, there is an exponential blowup as you give QuickSpec more functions to consider (though it doesn’t blow up as badly as you might think!)

  • QuickSpec only tests the laws, it doesn’t try to prove them. So while the generated laws are very likely to be true, there is still a chance that they are false, especially if your test data generation is not up to scratch.

Despite these limitations, QuickSpec works well on many examples.

This directory contains a new version of QuickSpec which is currently in flux - it works well, but has little documentation and the user interface is likely to change. If you look in the examples directory, you will find many examples which should help you on your way. Alternatively, if you check out the v1 branch of this repository, you will find an older version of QuickSpec, which is better-documented and slightly more polished, but worse at finding equations.