what4-1.6.3: Solver-agnostic symbolic values support for issuing queries

Copyright | (c) Galois Inc 2020
License | BSD3
Maintainer | kquick@galois.com
Safe Haskell | None
Language | Haskell2010

Test.Verification

Contents

- Testing definitions
- Test concretization

Description

This is a testing abstraction layer that allows the integration of test properties and functions into the What4 library without requiring a binding to a specific testing library or version thereof (e.g. QuickCheck, Hedgehog, etc.). All test properties and functions should be specified using the primary set of functions in this module, and then the actual test code will specify a binding of these abstractions to a specific test library.

In this way, the What4 can implement not only local tests but the test functionality can be exported to enable downstream modules to perform extended testing.

The actual tests should be written using only the functions exported in the testing exports section of this module. Note that only the set of functions needed for What4 is defined by this testing abstraction; if additional testing functions are needed, the GenEnv context should be extended to add an adaptation entry and the function should be defined here for use by the tests.

The overlap (common subset) between testing libraries such as QuickCheck and Hedgehog is only of moderate size: both libraries (and especially Hedgehog) provide functionality that is not present in the other library. This module does not attempt to provide full coverage for the functionality in both libraries; the intent is that test functions can be written using the proxy functions defined here and that downstream code using either of QuickCheck or Hedgehog can utilize these support functions in their own tests. As such, it is recommended that the What4 integrated tests are limited in expression to the common subset that can be described here.

A specific test configuration will need to use the functions and definitions in the concretization exports to bind these abstracted test functions to the specific library being used by that test suite.

For example, to bind to QuickCheck, specify:

    import QuickCheck
    import qualified Test.Verification as V

    quickCheckGenerators = V.GenEnv { V.genChooseBool = elements [ True, False ]
                                    , V.genChooseInteger = \r -> choose r
                                    , V.genChooseInt = \r -> choose r
                                    , V.genGetSize = getSize
                                    }

    genTest :: String -> V.Gen V.Property -> TestTree
    genTest nm p = testProperty nm
                   (property $ V.toNativeProperty quickCheckGenerators p)

Synopsis

- assuming :: Verifiable t => Bool -> t -> Property
- (==>) :: Verifiable t => Bool -> t -> Property
- property :: Bool -> Property
- chooseBool :: Gen Bool
- chooseInt :: (Int, Int) -> Gen Int
- chooseInteger :: (Integer, Integer) -> Gen Integer
- data Gen a
- getSize :: Gen Int
- class Verifiable prop where
  - verifying :: prop -> Property
- data Property
  - = BoolProperty Bool
  - | AssumptionProp Assumption
- data Assumption = Assuming {
  - preCondition :: Bool
  - assumedProp :: Property
  }
- data GenEnv (m :: Type -> Type) = GenEnv {
  - genChooseBool :: m Bool
  - genChooseInt :: (Int, Int) -> m Int
  - genChooseInteger :: (Integer, Integer) -> m Integer
  - genGetSize :: m Int
  }
- toNativeProperty :: Monad m => GenEnv m -> Gen b -> m b

# Testing definitions

These definitions should be used by the tests themselves. Most of these parallel a corresponding function in QuickCheck or Hedgehog, so the adaptation is minimal.

assuming :: Verifiable t => Bool -> t -> Property Source #

The named form of the `==>` assumption operator

(==>) :: Verifiable t => Bool -> t -> Property infixr 0 Source #

The assumption operator that performs the property test (second element) only when the first argument is true (the assumption guard for the test). This is the analog to the corresponding QuickCheck ==> operator.

property :: Bool -> Property Source #

Used by testing code to assert a boolean property.

chooseBool :: Gen Bool Source #

A test generator that returns True or False

chooseInt :: (Int, Int) -> Gen Int Source #

A test generator that returns an `Int` value between the specified (inclusive) bounds.

chooseInteger :: (Integer, Integer) -> Gen Integer Source #

A test generator that returns an `Integer` value between the specified (inclusive) bounds.

data Gen a Source #

This is the generator monad for the Verification proxy tests. The inner monad will be the actual test implementation's monadic generator, and the `a` return type is the type returned by running this monad.

Tests should only use the 'Gen TYPE' as an output; the constructors and internals should be used only by the test concretization.

#### Instances

Instances details

Applicative Gen Source # |
Instance details Defined in Test.Verification Methods pure :: a -> Gen a Source # (<*>) :: Gen (a -> b) -> Gen a -> Gen b Source # liftA2 :: (a -> b -> c) -> Gen a -> Gen b -> Gen c Source # (*>) :: Gen a -> Gen b -> Gen b Source # (<*) :: Gen a -> Gen b -> Gen a Source #
Functor Gen Source # |
Instance details Defined in Test.Verification Methods fmap :: (a -> b) -> Gen a -> Gen b Source # (<$) :: a -> Gen b -> Gen a Source #
Monad Gen Source # |
Instance details Defined in Test.Verification Methods (>>=) :: Gen a -> (a -> Gen b) -> Gen b Source # (>>) :: Gen a -> Gen b -> Gen b Source # return :: a -> Gen a Source #

getSize :: Gen Int Source #

A test generator that returns the current shrink size of the generator functionality.

class Verifiable prop where Source #

A class specifying things that can be verified by constructing a local Property.

Methods

verifying :: prop -> Property Source #

#### Instances

Instances details

Verifiable Property Source # |
Instance details Defined in Test.Verification Methods verifying :: Property -> Property Source #
Verifiable Bool Source # |
Instance details Defined in Test.Verification Methods verifying :: Bool -> Property Source #

# Test concretization

Used by test implementation functions to map from this Verification abstraction to the actual test mechanism (e.g. QuickCheck, HedgeHog, etc.)

data Property Source #

Local definition of a Property: intended to be a proxy for a QuickCheck Property or a Hedgehog Property. The `toNativeProperty` implementation function converts from these proxy Properties to the native Property implementation.

Tests should only use the `Property` type as an output; the constructors and internals should be used only by the test concretization.

Constructors

BoolProperty Bool |
AssumptionProp Assumption |

#### Instances

Instances details

Show Property Source # |
Instance details Defined in Test.Verification Methods showsPrec :: Int -> Property -> ShowS Source # show :: Property -> String Source # showList :: [Property] -> ShowS Source #
Verifiable Property Source # |
Instance details Defined in Test.Verification Methods verifying :: Property -> Property Source #

data Assumption Source #

Internal data structure to store the two elements to the `==>` assumption operator.

Constructors

Assuming |

Fields

- preCondition :: Bool
- assumedProp :: Property

#### Instances

Instances details

Show Assumption Source # |
Instance details Defined in Test.Verification Methods showsPrec :: Int -> Assumption -> ShowS Source # show :: Assumption -> String Source # showList :: [Assumption] -> ShowS Source #

data GenEnv (m :: Type -> Type) Source #

This is the reader environment for the surface level proxy testing monad. This environment will be provided by the actual test code to map these proxy operations to the specific testing implementation.

Constructors

GenEnv |

Fields

- genChooseBool :: m Bool
- genChooseInt :: (Int, Int) -> m Int
- genChooseInteger :: (Integer, Integer) -> m Integer
- genGetSize :: m Int

toNativeProperty :: Monad m => GenEnv m -> Gen b -> m b Source #

This function should be called by the testing code to convert the proxy tests in this module into the native tests (e.g. QuickCheck or Hedgehog). This function is provided with the mapping environment between the proxy tests here and the native equivalents, and a local Generator monad expression, returning a native Generator equivalent.