Пример, который показывает ограничения интегрированного сжатия - PullRequest
Новая
       72

Пример, который показывает ограничения интегрированного сжатия

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

Я только что посмотрел видео , которое представляет понятие интегрированного сжатия для тестов на основе свойств.Подход, кажется, имеет некоторые преимущества по сравнению с направленным сжатием типа , однако в этом реддитном потоке было отмечено, что интегрированный подход к сжатию не подходит для случая монадных генераторов:

Выполнение сжатия на вашем пути не подходит для монадического стиля для генераторов.Вот пример, рассмотрите возможность создания произвольного списка (пока игнорируйте завершение): 

do x <- arbitrary
   xs <- arbitrary
   return (x:xs)

Теперь поведение по умолчанию при вашем сжатии будет сначала уменьшать x (удерживая постоянную xs), а затем уменьшать xs (удерживаяx постоянная), которая сильно ограничивает сжатие (концепция локального минимума теперь намного менее сильна).

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

Ответы [ 2 ]

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

Просто для справки вот пример, который включает списки: 

{-# LANGUAGE OverloadedStrings #-}

module Main where

import Hedgehog
import qualified Hedgehog.Gen as Gen
import qualified Hedgehog.Range as Range

notLargeOrBothNotEmpty :: Property
notLargeOrBothNotEmpty = property $ do
  xs <- forAll randomIntLists
  ys <- forAll randomIntLists
  assert $ length xs < 4 && (xs /= [] && ys /=[])
  where
    randomIntLists = Gen.frequency
      [ (1, Gen.list (Range.constant 0 1) randomInt)
      , (10, Gen.list (Range.constant 1 100) randomInt)
      ]
    randomInt = Gen.integral (Range.constat 1 10)

main :: IO Bool
main = checkParallel $ 
  Group "Test.Example" [("Produce a minimal counter-example", notLargeOrBothNotEmpty)]

Так что ежик иногда возвращает в качестве контрпримеров списки ( [ 1 , 1 , 1 , 1 ], []).Однако ([], []) является меньшим контрпримером (о котором иногда также сообщает hedgehog).100

В этом случае условие, которое нарушает свойство: 

4 <= length xs || (xs == [] && ys == [])

Если изначально найден контрпример, где ys /= [] и 4 <= length xs, попытка интегрированного сокращениясначала уменьшите xs, а затем продолжите сжатие ys, сохраняя xs постоянным, как описано в посте, который я цитировал в своем первоначальном вопросе.

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

С точки зрения исчисления, проблема в том, что вы не следуете за отрицательным градиентом (самый крутой спуск), вместо этого вы сначала минимизируете вдоль 1 оси, а затем минимизируете вдоль другой оси.Основываясь на этой аналогии, легко придумать хотя бы надуманный пример - рассмотрим функцию 

-- f x y = ((x^2 - 1)^2 - 0.2*x) * ((y^2 - 1/2)^2 - 0.1*y)
f x y = (x^4 - 2.2*x^2 + 1) * (y^4 - 1.1*y^2 + 1/4)

См. График на WolframAlpha .

и мыповторно протестируем его для свойства f x y > 0, и скажем, минимальный пример будет иметь точку, ближайшую к началу координат (0, 0).В зависимости от того, где вы впервые начинаете сокращаться, вполне возможно, что вы окажетесь вблизи (±1, 0), потому что сначала вы настраиваете x, а затем не допускаете значительных изменений y.Однако в идеальной ситуации вы бы хотели оказаться где-то рядом с (0, ±1/2), чтобы удовлетворить критерию минимальности.

...