Сложность мышления свойств для FsCheck

Я начну с sndBigger - это очень простая функция, но вы можете написать некоторые свойства, которые должны содержать ее. Например, что происходит, когда вы меняете местами значения в кортеже:

// Reversing values of the tuple negates the result
let swap (a, b) = (b, a)
let prop_sndBiggerSwap x = 
  sndBigger x = not (sndBigger (swap x))

// If two elements of the tuple are same, it should give 'false'
let prop_sndBiggerEq a = 
  sndBigger (a, a) = false

EDIT: Это правило prop_sndBiggerSwap не всегда выполняется (см. Комментарий kvb ). Однако следующее должно быть правильным:

// Reversing values of the tuple negates the result
let prop_sndBiggerSwap a b = 
  if a <> b then 
    let x = (a, b)
    sndBigger x = not (sndBigger (swap x))

Что касается функции пар , kvb уже опубликовал несколько хороших идей. Кроме того, вы можете проверить, что преобразование преобразованного списка обратно в список элементов возвращает исходный список (вам нужно будет обработать случай, когда входной список нечетный - в зависимости от того, что должна выполнять функция pair сделать в этом случае):

let prop_pairsEq (x:_ list) = 
  if (x.Length%2 = 0) then
    x |> pairs |> List.collect (fun (a, b) -> [a; b]) = x
  else true

Для splitOn мы можем протестировать аналогичную вещь - если вы объедините все возвращенные списки, он должен дать исходный список (это не проверяет поведение разделения, но это хорошо для начала - он, по крайней мере, гарантирует, что никакие элементы не будут потеряны).

let prop_splitOnEq f x = 
  x |> splitOn f |> List.concat = x

Я не уверен, что FsCheck может справиться с этим (!), Потому что свойство принимает функцию в качестве аргумента (поэтому ему нужно будет генерировать «случайные функции»). Если это не сработает, вам нужно будет предоставить пару более конкретных свойств с помощью некоторой рукописной функции f .Затем реализовать проверку того, что f возвращает истину для всех соседних пар в разделенных списках (как предлагает kvb ), на самом деле не так уж и сложно:

let prop_splitOnAdjacentTrue f x = 
  x |> splitOn f 
    |> List.forall (fun l -> 
         l |> Seq.pairwise 
           |> Seq.forall (fun (a, b) -> f a b))

Вероятно, единственное последнее, что вы можете проверить, что f возвращает false , когда вы передаете ему последний элемент из одного списка и первый элемент из следующего списка. Нижеследующее не является полностью полным, но оно показывает, что нужно делать:

let prop_splitOnOtherFalse f x = 
  x |> splitOn f
    |> Seq.pairwise 
    |> Seq.forall (fun (a, b) -> lastElement a = firstElement b)

Последний пример также показывает, что вы должны проверить, может ли функция splitOn возвращать пустой список как часть возвращенного списка результаты (потому что в этом случае вы не смогли найти первый / последний элемент).

Для некоторого кода (например, sndBigger ) реализация настолько проста, что любое свойство будет не менее сложным, чем исходный код. , поэтому тестирование с помощью FsCheck может не иметь смысла. Однако для двух других функций вы можете проверить следующее:

• пары
  • Что ожидается, если исходная длина не делится на два? Вы можете проверить выброс исключения, если это правильное поведение.
  • List.map fst (пары x) = evenEntries x и List.map snd (pair x) = oddEntries x для простых функций evenEntries и oddEntries , который вы можете написать.
• splitOn
  • Если я понимаю ваше описание того, как функция должна работать, вы можете проверить такие условия, как «Для каждого списка в результате splitOn fl нет двух последовательных записей, удовлетворяющих f "и" Взятие списков (l1, l2) из , разделенных на fl попарно, выполняется f (последний l1) (первый l2) ». К сожалению, логика здесь, вероятно, будет сопоставима по сложности с самой реализацией.

Уже есть много конкретных ответов, поэтому я постараюсь дать некоторые общие ответы, которые могут дать вам некоторые идеи.

1. Индуктивные свойства рекурсивных функций. Для простых функций,это, вероятно, равносильно повторной реализации рекурсии. Однако сохраняйте простоту: в то время как фактическая реализация чаще всего развивается (например, она становится хвостовой рекурсивной, вы добавляете запоминаемую ,...), сохраняйте свойство простым. Здесь обычно пригодится комбинатор свойств ==>. Функция пар может стать хорошим примером.
2. Свойства, которые содержат несколько функций в модуле или типе. Обычно это происходит при проверке абстрактных типов данных. Например: добавление элемента в массив означает, что массив содержит этот элемент. Это проверяет согласованность Array.add и Array.contains.
3. Круговые поездки: это хорошо для преобразований (например, парсинга, сериализации) - сгенерировать произвольное представление, сериализовать его, десериализовать, проверить, что оно равно оригиналу. Вы можете сделать это с помощью splitOn и concat.
4. Общие свойства, как проверка на вменяемость. Ищите общеизвестные свойства, которые могут удерживаться - такие вещи, как коммутативность, ассоциативность, идемпотентность (применение чего-либо дважды не меняет результата), рефлексивности и т.д. Идея здесь больше в том, чтобы немного поупражнять функцию - посмотрите, делает ли она что-то действительно странное.

В качестве общего совета, постарайтесь не делать из этого слишком большой сделки. Для sndBigger хорошим свойством будет:

let ''should возвращает true тогда и только тогда, когда snd больше'' (a:int) (b:int) = sndBigger (a,b) = b > a

И это, вероятно, именно реализация. Не беспокойтесь об этом - иногда простой, старомодный модульный тест - это именно то, что вам нужно. Никакой вины не нужно! :)

Возможно, эта ссылка (от команды Pex) также дает некоторые идеи.