Maximilian Algehed

Quick, where is the spec?!

Maximilian got a PhD in software security from Chalmers University of Technology in Gothenburg, Sweden. After his PhD he chose to work at Quviq to help customers testing their difficult to test, critical software using property-based testing. At Quviq he has mainly been focussing on software written in Haskell. As he is a Haskell expert, he quickly helped to extend a variety of Haskell tools used in the software testing space.

QuickSpec: A Lightweight Theory Exploration Tool for Programmers

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.

Slides
Video ←Back