mirror of
https://github.com/nick8325/quickspec.git
synced 2024-09-11 08:35:32 +03:00
snapshot
This commit is contained in:
parent
7f45d03747
commit
5f731f4763
2
LICENSE
2
LICENSE
@ -1,4 +1,4 @@
|
||||
Copyright (c) 2009-2014, Nick Smallbone
|
||||
Copyright (c) 2009-2018, Nick Smallbone
|
||||
|
||||
All rights reserved.
|
||||
|
||||
|
@ -1,59 +0,0 @@
|
||||
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!
|
||||
|
||||
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.
|
||||
The best way to get started with it is to look at the `examples`
|
||||
directory, for example `Arith.hs`,`ListMonad.hs`, or `Parsing.hs`.
|
||||
You can also look at our paper,
|
||||
http://www.cse.chalmers.se/~nicsma/papers/quickspec2.pdf[Quick
|
||||
specifications for the busy programmer].
|
26
README.md
Normal file
26
README.md
Normal file
@ -0,0 +1,26 @@
|
||||
QuickSpec: equational laws for free!
|
||||
====================================
|
||||
|
||||
Ever get that nagging feeling that your code must satisfy some equational laws,
|
||||
but not sure what they are? Want to write some QuickCheck properties, but not
|
||||
sure where to start? QuickSpec might be for you! QuickSpec takes any set of
|
||||
Haskell functions and tries to discover laws about those functions.
|
||||
|
||||
Give QuickSpec the functions `reverse`, `++` and `[]`, for example, and it will
|
||||
find six laws:
|
||||
|
||||
```haskell
|
||||
reverse [] == []
|
||||
xs ++ [] == xs
|
||||
[] ++ xs == xs
|
||||
reverse (reverse xs) == xs
|
||||
(xs ++ ys) ++ zs == xs ++ (ys ++ zs)
|
||||
reverse xs ++ reverse ys == reverse (ys ++ xs)
|
||||
```
|
||||
|
||||
Despite these limitations, QuickSpec works well on many examples. The
|
||||
best way to get started with it is to look at the `examples` directory,
|
||||
for example `Arith.hs`,`ListMonad.hs`, or `Parsing.hs`. You can also
|
||||
look at our paper,
|
||||
http://www.cse.chalmers.se/\~nicsma/papers/quickspec2.pdf\[Quick
|
||||
specifications for the busy programmer\].
|
@ -8,6 +8,7 @@ eqLen :: [a] -> [b] -> Bool
|
||||
eqLen xs ys = length xs == length ys
|
||||
|
||||
main = quickSpec [
|
||||
-- Explore bigger terms.
|
||||
withMaxTermSize 8,
|
||||
withPruningDepth 10,
|
||||
con "++" ((++) @ Int),
|
||||
|
@ -9,7 +9,7 @@ Maintainer: nicsma@chalmers.se
|
||||
|
||||
License: BSD3
|
||||
License-file: LICENSE
|
||||
Copyright: 2009-2016 Nick Smallbone
|
||||
Copyright: 2009-2018 Nick Smallbone
|
||||
|
||||
Category: Testing
|
||||
|
||||
@ -90,16 +90,16 @@ library
|
||||
QuickSpec.Utils
|
||||
|
||||
Build-depends:
|
||||
QuickCheck >= 2.10,
|
||||
base >= 4 && < 5,
|
||||
constraints,
|
||||
containers,
|
||||
data-lens-light,
|
||||
dlist,
|
||||
random,
|
||||
reflection,
|
||||
spoon,
|
||||
template-haskell,
|
||||
transformers,
|
||||
twee-lib >= 2.1.1,
|
||||
uglymemo
|
||||
QuickCheck >= 2.10,
|
||||
base >= 4 && < 5,
|
||||
constraints,
|
||||
containers,
|
||||
data-lens-light,
|
||||
dlist,
|
||||
random,
|
||||
reflection,
|
||||
spoon,
|
||||
template-haskell,
|
||||
transformers,
|
||||
twee-lib >= 2.1.1,
|
||||
uglymemo
|
||||
|
Loading…
Reference in New Issue
Block a user