AlgebraCheckers

Model Checking

testModel :: ExpQ -> ExpQ

Generate QuickCheck property tests for the given model.

Examples

  lawTests :: [Property]
  lawTests = $(theoremsOf [e| do

  law "commutativity" $ a + b == b + a
  law "identity" (a + 0 == a)

  |])

theoremsOf :: ExpQ -> ExpQ

Like testModel, but also interactively dumps all of the derived theorems of your model. This is very helpful for finding dodgy derivations and outright contradictions.

Modeling Tools

law

Arguments

:: String

Name

-> Bool

Law. This is not any ordinary Bool! See the documentation on law for more information.

-> law

Asserts that an algebraic law must hold. This function must be called only in the context of either testModel or theoremsOf.

Any variables that appear in the Bool parameter are considered to be metavariables, and will be varied in the resulting property test.

The Bool parameter must be an expression of the form exp1 == exp2

Examples

law "set/get" $ set x (get x s) == s

law "set/set" (set x' (set x s) == set x' s)

homo

Arguments

:: (homo a, homo b)

=> (a -> b)

The function expected to be a homomorphism. This is not any ordinary function! See the documentation on homo for more information.

-> law

Asserts that a function should be a homomorphism in the argument described by a lambda.

This function must be called with a type application describing the desired homomorphism. Acceptable typeclasses are Semigroup, Monoid, Group, Eq and Ord.

The argument to this function must be a lambda binding a single variable.

This function introduces a law for every method in the typeclass.

This function must be called only in the context of either testModel or theoremsOf.

Examples

homo @Monoid $ \s -> set x s

notDodgy

Arguments

:: Bool

Law. This is not any ordinary Bool! See the documentation on law for more information.

-> law

Convinces theoremsOf that the following law is not dodgy, preventing it from appearing in the dodgy theorems list.

This function does not introduce a new law.

This function must be called only in the context of either testModel or theoremsOf.