GaloisInc/ivory — pull request #18 by gridaphobe (2014-12-06 00:20:44+00:00)
Title: Rewrite of ivory-quickcheck

This is a rewrite of `ivory-quickcheck` that generates inputs using the AST instead of the smart constructors, making it much easier to generate struct values. It also provides a higher-level API, basically

```haskell
-- | Generate a random C program to check that the property holds. The
-- generated program will be placed in the @test@ subdirectory.
check :: Int -- ^ The number of inputs to generate.
-> [Module] -- ^ Modules we need to have in scope.
-> Module -- ^ The defining module.
-> Def (args :-> IBool) -- ^ The property to check.
-> IO ()
```

and

```haskell
-- | Make a @check@able property from an arbitrary Ivory procedure. The
-- property will simply check that the contracts are satisfied.
contract :: Def (args :-> res) -> Def (args :-> IBool)
```

are the only functions a user should care about. You still have to compile and run the generated C program (with `-DIVORY_TEST`) yourself, and it could produce better errors than the standard C-assertion failure.

Furthermore, I've included a **very basic** ivory-eval package that implements just enough of an Ivory interpreter to evaluate the `requires` expressions so ivory-quickcheck can filter out inputs that don't satisfy the pre-conditions.