Cours 2

Htmligure
Version & licenses
Creative Commons License

QuickCheck

Guyslain
Thursday, 21 July 2016

Retour au sommaire.

QuickCheck.

Pour étudier les types paramétrés, nous allons utiliser l'exemple de QuickCheck. QuickCheck est une librairie qui permet de réaliser des tests automatisés de fonctions OCaml. Le principe est d'écrire une fonction prenant une valeur et un booléen, QuickCheck génére aléatoirement plein de valeurs différentes et teste la fonction avec, puis reporte s'il a trouvé une valeur pour laquelle la fonction retourne false.

Nous utiliserons QuickCheck tout au long du cours pour tester nos programmes, donc il est utile d'apprendre à l'utiliser immédiatement. Par ailleurs, QuickCheck repose sur plusieurs types paramétrés ayant différents rôles, ce qui permet bien d'illustrer les usages possibles des types paramétrés.

QuickCheck est un outil très complet, nous n'étudierons pas toutes ses fonctionnalités. À noter que QuickCheck est une adaptation d'une librairie Haskell du même nom, et qu'il en existe maintenant des versions dans de nombreux langages, par exemple en Java.

Un petit exemple.

Commençons par essayer sur un petit exemple, pour voir comment cela fonctionne.

  1. module Ratio =
  2. struct
  3. type t = (int * int)

  5. let zero = (0,1)
  6. let one = (1,1)

  8. let rec gcd n p =
  9. if p = 1 then n
  10. else gcd p (n mod p)

  12. let create n d =
  13. let p = gcd n d in
  14. let (n', d') = ( n/p, d/p ) in
  15. if d' < 0 then ( -n', -d')
  16. else (n', d')

  18. let ( +/ ) (n1,d1) (n2,d2) = create (n1+n2) (d1+d2)

  20. let ( */ ) (n1,d1) (n2,d2) = create (n1*n2) (d1*d2)

  22. let equals (n1,d1) (n2,d2) = n1 = n2 && d1 = d2

  24. let pp formatter (n,d) =
  25. Format.fprintf formatter "@[%d/%d@]" n d

  27. let to_string (n,d) =
  28. Printf.sprintf "%d/%d" n d
  29. end

Ce module permet de représenter les fractions (format : (numérateur, dénominateur)) et de faire des calculs avec. Malheureusement, il n'est pas correct. Nous allons utiliser QuickCheck pour trouver les erreurs et les corriger.

D'abord, nous allons charger QuickCheck dans l'interpréteur :

  1. #use "topfind";; (* allows to use #require *)
  2. #require "qcheck";; (* loads the quickcheck package *)
  3. #install_printer Ratio.pp;;
  4. (* allows the interpreter to write the ratios in a pretty way *)

Ensuite, nous allons écrire quelques propriétés qui doivent être vérifiés par les fonctions que nous avons définies. En voici un petit échantillon, qui utilise les propriétés de bases d'une algèbre :

  1. let gcd_is_common_divisor (n,p) =
  2. let d = Ratio.gcd n p in
  3. n mod d = 0 && p mod d = 0

  5. let gcd_with_a_multiple_is_itself (n,p) =
  6. Ratio.gcd n (p * n) = n

  8. let zero_is_addition_neutral ratio =
  9. Ratio.(equals (ratio +/ zero) ratio)
  10. && Ratio.(equals (zero +/ ratio) ratio)

  12. let addition_is_commutative (ratio1,ratio2) =
  13. Ratio.(equals (ratio1 +/ ratio2) (ratio2 +/ ratio1))

  15. let addition_is_associative (ratio1, ratio2, ratio3) =
  16. Ratio.(equals
  17. (ratio1 +/ (ratio2 +/ ratio3))
  18. ((ratio1 +/ ratio2) +/ ratio3)
  19. )

  21. let one_is_multiplication_neutral ratio =
  22. Ratio.(equals (ratio */ one) ratio)
  23. && Ratio.(equals (one */ ratio) ratio)

  25. let multiplication_is_distributive (ratio1, ratio2, ratio3) =
  26. Ratio.(equals
  27. ((ratio1 +/ ratio2) */ ratio3)
  28. (ratio1 */ ratio3 +/ ratio2 */ ratio3)
  29. )

QuickCheck génère des tests aléatoirement, nous devons lui apprendre à générer une fraction aléatoirement.

  1. let shrink_ratio (n,d) =
  2. let open QCheck.Iter in
  3. (if n <> 0 then return (Ratio.create (n/2) d) else empty)
  4. <+>
  5. (if d > 1 then return (Ratio.create n ((d + 1) / 2)) else empty)

  7. let ratio_gen =
  8. let open QCheck.Gen in
  9. pair (-1000 -- 1000) (1 -- 1000)
  10. |> map (fun (n,d) -> Ratio.create n d)

  12. let ratio_arbitrary : Ratio.t QCheck.arbitrary =
  13. QCheck.make
  14. ~print:Ratio.to_string
  15. ~shrink:ratio_shrink
  16. ratio_gen

QCheck.arbitrary est un type paramétré pour les générateurs aléatoires de valeurs utilisés par QuickCheck. ratio_arbitrary a donc le type d'un générateur de fractions, ce que l'on voulait. Son code est pour l'instant magique, on l'expliquera plus tard.

Il nous faut aussi un générateur de paires d'entiers pour tester la fonction de pgcd. Le voilà :

  1. let int_pair_arbitrary : (int * int) QCheck.arbitrary =
  2. QCheck.(pair small_int small_int)

À nouveau, le type paramétré de int_pair_arbitrary correspond à ce que nous désirons.

Commençons donc par tester le calcul de pgcd.

  1. # let test_gcd =
  2. QCheck.Test.make
  3. ~name:"Test common divisor"
  4. int_pair_arbitrary
  5. gcd_is_common_divisor
  6. |> QCheck.Test.check_exn;;

  8. Exception:
  9. QCheck.Test.Test_fail ("Test common divisor",
  10. ["(0, 0) (after 16 shrink steps)"]).

Il trouve donc un erreur (Test_fail), pour la paire (0,0). Il indique aussi avoir fait 16 étapes de réductions : il essaie toujours de trouver un plus petit contre-exemple possible, en utilisant des règles de simplifications sur les contre-exemples. On vérifie maintenant l'erreur pour essayer de la comprendre :

  1. # let res = Ratio.gcd 0 0;;
  2. Exception: Division_by_zero.

Une division par zéro ! on corrige donc l'algorithme de pgcd, en remplaçant le test p = 1 par p = 0, qui est le bon cas de base.

Reprenons les tests :

  1. # let test_common_divisor =
  2. QCheck.Test.make
  3. ~name:"test common divisor"
  4. int_pair_arbitrary
  5. gcd_is_common_denominator
  6. |> QCheck.Test.check_exn

  8. # let test_divisor_of_multiples =
  9. QCheck.Test.make
  10. ~name:"test divisor of multiples"
  11. int_pair_arbitrary
  12. gcd_with_a_multiple_is_itself
  13. |> QCheck.Test.check_exn

  15. # let test_zero_neutral =
  16. QCheck.Test.make
  17. ~name:"test zero neutral"
  18. ratio_arbitrary
  19. zero_is_addition_neutral
  20. |> QCheck.Test.check_exn

  22. Exception:
  23. QCheck.Test.Test_fail ("test zero neutral",
  24. ["-1/1 (after 12 shrink steps)"]).

Le calcul du pgcd semble être corrigé. Par contre l'addition n'est pas bonne, puisque zéro ne semble pas être neutre. Faisons le calcul :

  1. # Ratio.(create (-1) 1 +/ zero);;
  2. - : Ratio.t = -1/2

C'est effectivement clairement faux. La raison est simple, le code de l'addition est complètement faux, n'importe quel collégien s'en rendrait compte... On le corrige :

  1. let ( +/ ) (n1,d1) (n2,d2) = ( n1*d2 + n2*d1, d1*d2)

Puis on continue de tester :

  1. let test_addition_is_commutative =
  2. QCheck.Test.make
  3. ~name:"test addition commutative"
  4. QCheck.(pair ratio_arbitrary ratio_arbitrary)
  5. addition_is_commutative
  6. |> QCheck.Test.check_exn

  8. let test_addition_is_associative =
  9. QCheck.Test.make
  10. ~name:"test addition associative"
  11. QCheck.(triple ratio_arbitrary ratio_arbitrary ratio_arbitrary)
  12. addition_is_associative
  13. |> QCheck.Test.check_exn

  15. let test_one_neutral =
  16. QCheck.Test.make
  17. ~name:"Test one neutral"
  18. ratio_arbitrary
  19. one_is_multiplication_neutral
  20. |> QCheck.Test.check_exn

Les trois tests suivants passent sans problème. Pour tester la commutativité de l'addition, il faut deux fractions. Le deuxième argument de QCheck.Test.make précise donc qu'il faut tirer des paires de fractions. De même pour l'associativité de l'addition, on tire des triplets de fractions.

Le dernier test pose problème :

  1. # let test_multiplication_is_distributive =
  2. QCheck.Test.make
  3. ~name:"test multiplication distributive"
  4. QCheck.(triple ratio_arbitrary ratio_arbitrary ratio_arbitrary)
  5. multiplication_is_distributive
  6. |> QCheck.Test.check_exn;;

  8. Exception:
  9. QCheck.Test.Test_fail ("test multiplication distributive",
  10. ["(-1/1, -1/1, -1/2) (after 43 shrink steps)"]).

Regardons ce qui se passe :

  1. # let _ =
  2. let ratio1 = Ratio.create (-1) 1 in
  3. let ratio2 = Ratio.create (-1) 1 in
  4. let ratio3 = Ratio.create (-1) 2 in
  5. ( Ratio.( (ratio1 +/ ratio2) */ ratio3 ),
  6. Ratio.( ratio1 */ ratio3 +/ ratio2 */ ratio3)
  7. );;
  8. - : Ratio.t * Ratio.t = (1/1, 4/4)

Les deux fractions sont égales, mais la deuxième n'est pas sous forme canonique. Normalement tous les fractions doivent être mises sous forme canonique à leur création. Le problème vient de l'addition, qui n'a pas simplifié le résultat du second calcul. Il faut passer par create pour écrire l'addition.

On obtient alors le module suivant, qui passe tous les tests, et dont on peut humblement espérer qu'il soit enfin sans erreur.

  1. module Ratio =
  2. struct
  3. type t = (int * int)

  5. let zero = (0,1)
  6. let one = (1,1)

  8. let rec gcd n p =
  9. if p = 0 then n
  10. else gcd p (n mod p)

  12. let create n d =
  13. let p = gcd n d in
  14. let (n', d') = (n/p, d/p) in
  15. if d' < 0 then (-n', -d')
  16. else (n', d')

  18. let ( +/ ) (n1,d1) (n2,d2) = create (n1*d2 + n2*d1) (d1*d2)

  20. let ( */ ) (n1,d1) (n2,d2) = create (n1*n2) (d1*d2)

  22. let equals (n1,d1) (n2,d2) = n1 = n2 && d1 = d2

  24. let pp formatter (n,d) =
  25. Format.fprintf formatter "@[%d/%d@]" n d

  27. let to_string (n,d) =
  28. Printf.sprintf "%d/%d" n d
  29. end

Récapitulatif.

QuickCheck est un outil de génération automatique d'instances pour réaliser des tests unitaires. Pour réaliser un test il faut :

  1. écrire un fonction à un argument et retournant un booléen,
  2. écrire un générateur, de type arg QuickCheck.arbitrary,
  3. utiliser la fonction QuickCheck.Test.make, avec en argument le générateur et la fonction à tester, ce qui crée le test,
  4. appeler la fonction QuickCheck.Test.check_exn sur le test, ce qui provoque son exécution.

QuickCheck génère des tests, les fait passer, simplifie automatiquement les contre-exemples et reporte le résultat. Nous l'utiliserons dorénavant et pour tout le semestre pour vérifier nos programmes.

QuickCheck utilise plusieurs types paramétrés :

  • Gen.t le type des générateurs aléatoires,
  • Print.t le type des conversions en chaînes de caractères,
  • Iter.t qui permet de décrire les réductions possibles d'une instance,
  • Shrink.t qui représente les fonctions de réductions,
  • arbitrary le type des générateurs d'instances.
  • Test.cell qui représente un test unitaire.

Tous ces types ne s'utilisent pas de la même façon, mais rentrent dans trois grandes classes de types paramétrés possibles. C'est ce que nous allons détailler.

Retour au sommaire.