Last updated: 2015-01-27 18:03:56 +0100
Upstream URL: git clone http://chriswarbo.net/git/hipspec.git
Contents of README.md follows
HipSpec is an inductive theorem prover for Haskell programs. It will (try to) conjecture essential lemmas to prove tricky properties. It supports all algebraic Haskell 98 data types and polymorphism. We assume that functions terminate on finite input and produce finite output. All quantification is only over total and finite values.
In the <code>examples/Rotate.hs</code> file we see the following definitions:
<pre><code>rotate :: Nat -> [a] -> [a] rotate Z xs = xs rotate _ [] = [] rotate (S n) (x:xs) = rotate n (xs ++ [x]) prop_rotate :: [a] -> Prop [a] prop_rotate xs = rotate (length xs) xs =:= xs</code></pre>The second definition defines a property in the HipSpec property language that we would like to prove. The <code>=:=</code> operator simply means equals.
Let’s run HipSpec on this file:
<pre><code>$ hipspec Rotate.hs --auto --cg --verbosity=30 Depth 1: 11 terms, 5 tests, 29 evaluations, 11 classes, 0 raw equations. Depth 2: 63 terms, 100 tests, 2151 evaluations, 48 classes, 15 raw equations. Depth 3: 1688 terms, 100 tests, 63851 evaluations, 1303 classes, 385 raw equations. Proved xs++[] == xs by induction on xs using Z3 Proved (xs++ys)++zs == xs++(ys++zs) by induction on xs using Z3 Proved length (xs++ys) == length (ys++xs) by induction on ys,xs using Z3 Proved rotate m [] == [] without induction using Z3 Proved rotate m (rotate n xs) == rotate n (rotate m xs) by induction on n,m using Z3 Proved rotate (S m) (rotate n xs) == rotate (S n) (rotate m xs) by induction on xs using Z3 Proved rotate m (x:[]) == x:[] by induction on m using Z3 Proved rotate m xs++rotate m xs == rotate m (xs++xs) by induction on m using Z3 Proved length (rotate m xs) == length xs by induction on m using Z3 Proved rotate (length xs) (xs++ys) == ys++xs by induction on xs using Z3 Proved prop_rotate {- rotate (length xs) xs == xs -} without induction using Z3 Proved: xs++[] == xs (xs++ys)++zs == xs++(ys++zs) length (xs++ys) == length (ys++xs) rotate m (rotate n xs) == rotate n (rotate m xs) rotate (S m) (rotate n xs) == rotate (S n) (rotate m xs) rotate m (x:[]) == x:[] rotate m xs++rotate m xs == rotate m (xs++xs) length (rotate m xs) == length xs rotate (length xs) (xs++ys) == ys++xs prop_rotate {- rotate (length xs) xs == xs -}</code></pre>The property and some lemmas conjectured by QuickSpec have been proved! Success!
HipSpec is maintained for GHC 7.8.3.
If you have an older version of GHC and cannot upgrade, try building at commit 2ba4d52c2c101a810dea4058496cf5f0da199b31.
You need to have the development version of QuickSpec. It can be obtained by cloning that repository:
<pre><code>git clone https://github.com/nick8325/quickspec</code></pre>Assuming your directory structure looks like this:
<pre><code>$CWD/ hipspec/ ... quickspec/ ...</code></pre>You current directory is $CWD. You can then install quickspec and hipspec in one go, which makes the dependency analysis better:
<pre><code>cabal install hipspec/ quickspec/</code></pre>The <code>homebrew</code> program sometimes messes up the package <code>ghc-paths</code>. If you get the error that <code>hipspec</code> cannot find the <code>HipSpec</code> module, try to reinstall this package with:
<pre><code>cabal install ghc-paths --reinstall</code></pre>We support:
<ul> <li>Z3. The default.</li> <li>CVC4.</li> <li>Alt Ergo, in particular versions 0.94 and 0.95. It exists in the ubuntu repositories, and in Arch Linux’ AUR.</li> <li>vampire, but your executable should be called <code>vampire-rel</code> (or change <code>src/HipSpec/ATP/Provers.hs</code>).</li> <li>E</li> <li>SPASS</li> </ul>See <code>--help</code> to see the flags to select theorem provers.
HipSpec can generate a signature for you with the <code>--auto</code> flag. If you want to see what signature it generated for you, use the <code>--print-auto-sig</code> flag. Unfortunately, the monomorphiser is not very clever yet: say you have lists in your program, then <code>(:)</code> will only get the type <code>A -> [A] -> [A]</code> and not other presumably desireable instances such as <code>[A] -> [[A]] -> [[A]]</code> and <code>Nat -> [Nat] -> [Nat]</code>.
To make HipSpec print a small, pruned theory of everything that is proved to be correct, run the compiled binary with <code>--explore-theory</code>, or <code>-e</code> for short.
Quick information about available flags can be accessed anytime by the <code>--help</code> flag to the <code>hipspec</code> executable.
While theorem provers are still usually single-core, you can run many of them in parallel. The <code>--processes</code> or <code>-N</code> flag will let you specify this. The default is 2, but if you to use eight cores: <code>-N=8</code>.
The default timeout is one second. It can be specified with the <code>-t</code> or <code>--timeout</code> flag. With <code>-t=5</code>, each theorem prover invocation will be 5 seconds long. The timeout can be issued as a double, so <code>-t=0.25</code> can be used to get 250 ms timeout.
Should you wish to inspect the generated theory, you can use <code>--output</code> (or <code>-o</code>) to make a <code>proving/</code> directory. Then all relevant files will be put there for you to view.
The HipSpec group consists of:
<ul> <li>Dan Rosén, danr@chalmers.se,
</li> <li>Koen Claessen
</li> <li>Moa Johansson
</li> <li>Nicholas Smallbone
</li> </ul>