Quick specifications for the busy programmer. (10th July 2017)

• Record Type: Journal Article
• Authors: SMALLBONE, NICHOLAS; JOHANSSON, MOA; CLAESSEN, KOEN; ALGEHED, MAXIMILIAN
• Is Part Of: Journal of functional programming. Volume 27(2017)
• Publication Date: 2017-07-10
• Subjects: Functional programming (Computer science) -- Periodicals
• DOI: 10.1017/S0956796817000090
• Languages: English
• ISSNs: 0956-7968

Abstract

Abstract: QuickSpec is a theory exploration system which tests a Haskell program to find equational properties of it, automatically. The equations can be used to help understand the program, or as lemmas to help prove the program correct. QuickSpec is largely automatic: the user just supplies the functions to be tested and QuickCheck data generators. Previous theory exploration systems, including earlier versions of QuickSpec itself, scaled poorly. This paper describes a new architecture for theory exploration with which we can find vastly more complex laws than before, and much faster. We demonstrate theory exploration in QuickSpec on problems both from functional programming and mathematics.