CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Quick Specifications for the Busy Programmer

Nicholas Smallbone (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Moa Johansson (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Koen Claessen (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Maximilian Algehed (Institutionen för data- och informationsteknik (Chalmers))
Journal of functional programming (0956-7968). Vol. 27 (2017),
[Artikel, refereegranskad vetenskaplig]

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.



Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2016-12-15. Senast ändrad 2017-08-16.
CPL Pubid: 246148

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)