Ivory.QuickCheck

Check properties of Ivory programs using random inputs.

Example usage:

[ivory|
struct foo
  { foo_a :: Stored IFloat
  ; foo_b :: Stored Uint8
  }
|]

-- Function we want to generate inputs for.
func :: Def ('[ Uint8
              , Ref s (Array 3 (Stored Uint8))
              , Ref s (Struct "foo")
              ] :-> ())
func = proc "func" $ \u arr str ->
  ensures_ (checkStored (arr ! 0) (\r -> r >? u)) $
  body $
  arrayMap $ \ix -> do
    a <- deref (arr ! ix)
    b <- deref (str ~> foo_b)
    store (arr ! ix) (a + b + u)

-- Module containing our function
cmodule :: Module
cmodule = package "module" $ do
  defStruct (Proxy :: Proxy "foo")
  incl func

-- Running @mkTest@ will produce a C program in @<pwd>/test@ that will check
-- @func@'s contract on 10 random inputs.
mkTest :: IO ()
mkTest = check 10 [] cmodule (contract func)

Documentation

check

Arguments

:: 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 ()

Generate a random C program to check that the property holds. The generated program will be placed in the test subdirectory.

checkWith

Arguments

:: Int

The number of inputs to generate.

-> Opts

Options to pass to the Ivory compiler.

-> [Module]

Modules we need to have in scope.

-> Module

The defining module.

-> Def (args :-> IBool)

The property to check.

-> IO ()

Generate a random C program to check that the property holds. The generated program will be placed in the test subdirectory.

contract :: Def (args :-> res) -> Def (args :-> IBool)

Make a checkable property from an arbitrary Ivory procedure. The property will simply check that the contracts are satisfied.