Difficoltà a pensare alle proprietà per FsCheck

Question

Sono riuscito a ottenere lavorando sul mio piccolo campionario. Ora voglio vedere se riesco a frullare anche FsCheck. Il mio problema è che sono perplesso quando si tratta di definire le proprietà di test per le mie funzioni.

Forse non ho un buon insieme di funzioni di esempio, ma quali sarebbero le buone proprietà di test per queste funzioni, ad esempio?

//transforms [1;2;3;4] into [(1,2);(3,4)] 
pairs : 'a list -> ('a * 'a) list  //' 

//splits list into list of lists when predicate returns 
// true for adjacent elements 
splitOn : ('a -> 'a -> bool) -> 'a list -> 'a list list 

//returns true if snd is bigger 
sndBigger : ('a * 'a) -> bool (requires comparison) 

Answer 1

Per qualche codice (ad esempio sndBigger), l'applicazione è così semplice che qualsiasi proprietà sarà almeno così complesso come il codice originale, in modo test tramite FsCheck potrebbe non avere senso. Tuttavia, per le altre due funzioni qui ci sono alcune cose che si potrebbe verificare:

• pairs
  • cosa ci si aspetta quando la lunghezza originale non è divisibile per due? È possibile verificare la presenza di un'eccezione se questo è il comportamento corretto.
  • List.map fst (pairs x) = evenEntries x e List.map snd (pairs x) = oddEntries x per le funzioni semplici evenEntries e oddEntries che è possibile scrivere.
• splitOn
  • Se ho ben capito la tua descrizione di come si suppone che la funzione di lavorare, allora si potrebbe verificare le condizioni del tipo "Per ogni lista nel risultato di splitOn f l, non ci sono due voci consecutive soddisfare f" e "Prendendo le liste (l1,l2) da splitOn f l a coppie, f (last l1) (first l2) tiene". Sfortunatamente, la logica qui sarà probabilmente comparabile in complessità all'implementazione stessa.

Answer 2

Comincerò con sndBigger - si tratta di una funzione molto semplice, ma è possibile scrivere alcune proprietà che dovrebbero tenere su di esso. Per esempio, cosa succede quando si invertire i valori nella tupla:

// 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: Questa regola prop_sndBiggerSwap non sempre avviene (vedi commento di KVB ). Tuttavia il seguente dovrebbe essere corretta:

// 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)) 

Per quanto riguarda la funzione di pairs, KVB già postato alcune buone idee. Inoltre, è possibile controllare che riportare l'elenco trasformato in un elenco di elementi restituisca l'elenco originale (sarà necessario gestire il caso quando l'elenco di input è dispari, a seconda di cosa dovrebbe fare la funzione pairs in questo caso):

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

per splitOn, possiamo testare cosa simile - se concatenare tutte le liste restituite, dovrebbe dare la lista originale (questo non consente di verificare il comportamento scissione, ma è una buona cosa per cominciare - almeno garantisce che nessun elemento sarà perso).

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

io non sono sicuro se FsCheck in grado di gestire questo però (!) Perché la proprietà prende una funzione come argomento (per cui sarebbe necessario generare "funzioni casuali"). Se questo non funziona, dovrai fornire un paio di proprietà più specifiche con alcune funzioni scritte a mano f. Successivamente, l'attuazione del controllo che f restituisce vero per tutte le coppie adiacenti negli elenchi a spacco (come KVB suggerisce) in realtà non è poi così difficile:

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

Probabilmente l'unica ultima cosa che si potrebbe verificare è che f restituisce false quando gli si assegna l'ultimo elemento da una lista e il primo elemento dall'elenco successivo. Quanto segue non è del tutto completa, ma mostra la strada da percorrere:

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

L'ultimo esempio mostra anche che si dovrebbe verificare se la funzione splitOn può restituire un elenco vuoto come parte della lista restituita dei risultati (perché in quel caso, non potresti trovare il primo/ultimo elemento).

Answer 3

Ci sono già molte risposte specifiche, quindi cercherò di dare alcune risposte generali che potrebbero darti qualche idea.

1. Proprietà induttive per funzioni ricorsive. Per le funzioni semplici, ciò equivale probabilmente a riattivare la ricorsione. Tuttavia, mantienilo semplice: mentre l'implementazione effettiva molto più spesso di quanto non evolva (ad esempio diventa coda ricorsiva, aggiungi la memoizzazione, ...) mantieni la proprietà semplice. Il ==> combinatore di proprietà di solito è utile qui. La tua funzione di coppia potrebbe essere un buon esempio.
2. Proprietà che contengono più funzioni in un modulo o un tipo. Questo di solito è il caso quando si controllano i tipi di dati astratti. Ad esempio: aggiungere un elemento a un array significa che l'array contiene quell'elemento. Controlla la coerenza di Array.add e Array.contains.
3. Round trip: questo è utile per le conversioni (ad esempio analisi, serializzazione): genera una rappresentazione arbitraria, serializza, deserializza, controlla che sia uguale all'originale. Potrebbe essere possibile farlo con splitOn e concat.
4. Proprietà generali come controlli di integrità. Cerca le proprietà generalmente conosciute che possono contenere: cose come commutabilità, associatività, idempotenza (applicare qualcosa per due volte non cambia il risultato), riflessività, ecc. L'idea qui è più di esercitare un po 'la funzione - vedi se fa qualcosa di davvero strano .

Come consiglio generale, cerca di non trarne un grosso problema. Per sndBigger, una buona proprietà sarebbe:

lasciare `` deve restituire true se e solo se snd è più grande`` (a: int) (b: int) = sndBigger (a, b) = b> a

E questa è probabilmente esattamente l'implementazione. Non preoccuparti: a volte un semplice test unitario vecchio stile è proprio quello di cui hai bisogno. Nessun senso di colpa necessario! :)

Forse this link (dal team Pex) dà anche alcune idee.