Maximilian Algehed

Quick, where is the spec?!

Functional Programming Fundamentalist at Chalmers

QuickSpec is a tool that automatically finds equations for a given signature of Haskell functions. For example, when running QuickSpec on the functions reverse and, the tool automatically finds the following equations:

rev (rev xs) ≡ xs
xs + (ys + zs) ≡ (xs + ys) + zs rev (xs+ys) ≡rev ys+rev xs

When the signature is extended to include the function zip, QuickSpec finds the additional equations:

zip xs (xs + ys) ≡ zip xs xs
zip (xs +ys) xs ≡ zip xs xs
zip (rev xs) (rev xs) ≡ rev (zip xs xs) rev (zip xs (rev xs)) ≡ zip (rev xs) xs

These equations are found by means of random testing, not by theorem proving. QuickSpec thus conjectures equations that could later be proven correct by other means.

QuickSpec’s big success so far has been its use in automated theorem proving by induction. We also believe QuickSpec to be a useful tool for Haskell programmers. Specifications generated by QuickSpec provide a good start for producing manual equational specifications of a module. The fact that QuickSpec is based on testing makes it suitable for use on large and complicated Haskell modules. Our demo will show QuickSpec in action and demonstrate some recent features. We will focus on the recent extension which lets QuickSpec handle conditional equations. We aim to make the demo interactive, for example by letting the audience suggest interesting functions for QuickSpec to explore.



For general info:
To become a sponsor: