Какова наилучшая практика для создания данных, которые удовлетворяют определенному свойству в QuickCheck? - PullRequest
Новая
       71

Какова наилучшая практика для создания данных, которые удовлетворяют определенному свойству в QuickCheck?

0 голосов
/ 10 января 2019

Когда мы используем QuickCheck для проверки наших программ, нам нужно определить генераторы для наших данных, есть некоторый общий способ их определения, но общий способ обычно становится бесполезным, когда нам нужны сгенерированные данные для удовлетворения некоторых ограничений для работы .

, например 

data Expr
    = LitI Int
    | LitB Bool
    | Add Expr Expr
    | And Expr Expr

data TyRep = Number | Boolean

typeInfer :: Expr -> Maybe TyRep
typeInfer e = case e of
    LitI _ -> Number
    LitB _ -> Boolean
    Add e1 e2 -> case (typeInfer e1, typeInfer e2) of
        (Just Number, Just Number) -> Just Number
        _ -> Nothing
    And e1 e2 -> case (typeInfer e1, typeInfer e2) of
        (Just Boolean, Just Boolean) -> Just Boolean
        _ -> Nothing

Теперь мне нужно определить генератор Expr (т.е. Gen Expr или instance Arbitrary Expr), но также хочу, чтобы он генерировал корректные типы (т.е. isJust (typeInfer generatedExpr))

Наивный способ сделать это - использовать suchThat, чтобы отфильтровать недействительные, но это, очевидно, неэффективно, когда Expr и TyRep усложняются с большим количеством случаев.

Другая похожая ситуация касается ссылочной целостности, например 

data Expr
    = LitI Int
    | LitB Bool
    | Add Expr Expr
    | And Expr Expr
    | Ref String -- ^ reference another Expr via it's name

type Context = Map String Expr

В этом случае мы хотим, чтобы все ссылочные имена в сгенерированном Expr содержались в каком-то конкретном Context, теперь мне нужно сгенерировать Expr для конкретного Context: 

arbExpr :: Context -> Gen Expr

, но теперь проблема с усадкой будет проблемой, и чтобы решить эту проблему, я должен определить конкретную версию сжатия и использовать forAllShrink каждый раз, когда я использую arbExpr, что означает большую работу.

Итак, я хочу знать, есть ли лучшая практика для таких вещей?

1 Ответ

0 голосов
/ 10 января 2019

Для хорошо типизированных терминов во многих случаях простой подход состоит в том, чтобы иметь один генератор для каждого типа или, что эквивалентно, функцию TyRep -> Gen Expr. Добавляя переменные поверх этого, это обычно превращается в функцию Context -> TyRep -> Gen Expr.

В случае генерации терминов с переменными (и с отсутствующими или очень простыми типами), индексирование типа терминов по контексту (например, как вы это делаете, используя библиотеку bound) должно облегчить получение генератор в общем.

Для сжатия подход hedgehog может работать довольно хорошо, где Gen генерирует значение вместе с сокращенными версиями, избавляя вас от определения отдельной функции сжатия.

Обратите внимание, что по мере того, как соотношение правильности и типизации становится более сложным, вы начинаете сталкиваться с теоретической стеной, где генерирование терминов, по крайней мере, так же сложно, как и произвольный поиск доказательства.

Для более продвинутой техники / связанной литературы, с моими собственными комментариями о возможном использовании ее в Haskell:

  • Создание ограниченных данных с равномерным распределением , автор Claessen et al., FLOPS'14 ( PDF ). Я полагаю, что пакет Haskell lazy-search имеет большую часть машин, описанных в статье, но, похоже, он нацелен на перечисление, а не на случайную генерацию.

  • Создание случайных суждений: автоматическое создание хорошо типизированных терминов из определения системы типов , Фетшер и др., ESOP'15 ( PDF ), название говорит само за себя. Я не знаю о реализации на Haskell; Вы можете спросить авторов.

  • Удача новичка: язык для генераторов на основе свойств , Лампропулос и др., POPL'17 ( PDF ) (отказ от ответственности: я соавтор) , Язык свойств (точнее, функций T -> Bool, например, средство проверки типов), которые можно интерпретировать как случайные генераторы (Gen T). Синтаксис языка сильно вдохновлен Haskell, но есть еще несколько отличий. Реализация имеет интерфейс для извлечения сгенерированных значений в Haskell ( github repo ).

  • Генерация хороших генераторов для индуктивных отношений , Lampropoulos et al. POPL'18 ( PDF ). Он находится в Coq QuickChick, но привязка его к Haskell QuickCheck путем извлечения кажется вполне осуществимой.

...