SmallCheck generate data satisfying invariants

2019-06-05 05:02发布

问题:

I want to use SmallCheck to test my code. I managed to generate arbitrary lists of pairs of ints, but that's not what my type should contain. The list represents a set of ranges, where [1,3),[4,6) would be encoded/stored as [(1,3),(4,6)].

These are the invariants for the normalized form of my ranges:

fst a < snd a 
snd a < fst b where a is before b in the list

I would like to communicate this to SmallCheck so that it doesn't generate loads of values that I throw away, because they aren't satisfying my invariants, but maybe that's not possible.

How can I generate lists satisfying my invariants?

回答1:

Favour application-specific types over built-int types (Int, List). This is advice not just for SmallCheck, but for any piece of software, in any language.

data Interval = Interval (Int,Int)
data Domain = Domain [Interval]

Write smart constructors that enforce your invariants.

interval :: Int -> Int -> Interval
interval x y = Interval (min x y, max x y) -- if you want this

domain :: [Interval] -> Domain
domain ints = Domain ... (something that sorts intervals, and perhaps merges them)

Then use these to create Serial instances.



回答2:

I do agree that this problem is solved better with user-defined types.

I assume you are writing an algorithm that has some property for disjoint half-open intervals sorted in an ascending order, then the following provides Serial instances.

I decided to give Interval and AscDisjIntervals different generators rather than implementing one in terms of the other.

The algorithm for AscDisjIntervals is as I already wrote in the comment

  • generating a list of non-negative Integers (this is to avoid Int overflow)
  • summing these integers (this asserts an ascending order of all values
  • generating pairs from this list (discarding the last single element if the list has an odd number of elements)

Intervals.hs

{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses #-}
module Intervals where

newtype Interval = I (Integer,Integer) deriving(Eq)

instance Show Interval where
    show (I (a,b)) = "["++show a ++ ", "++ show b ++ "]"

instance Monad m => Serial m Interval where
    series = let a_b a b = I (getNonNegative $ min a b , getNonNegative $ max a b) 
             in cons2 a_b

newtype AscDisjIntervals = ADI [Interval] deriving (Eq)

instance Show AscDisjIntervals where
    show (ADI x) = "|- "++ (unwords $ map show x) ++ " ->"

instance Monad m => Serial m AscDisjIntervals where
    series = cons1 aux1

aux1 :: [NonNegative Int] -> AscDisjIntervals
aux1 xx = ADI . generator . tail $ scanl (+) 0 xx
  where generator [] = []
        generator (_:[]) = []
        generator (x:y:xs) = let i = I (getNonNegative x ,getNonNegative y)
                        in i:generator xs

Note: I only compiled the program and did not test any properties.