Le sombre état des bibliothèques de tests property-based

 (stevana.github.io)
1 points par GN⁺ 2024-07-06 | 1 commentaires | Partager sur WhatsApp
  • Le property-based testing s’est diffusé dans plusieurs langages après QuickCheck, mais en juillet 2024, de nombreuses bibliothèques ne fournissent toujours pas correctement les tests stateful et les tests parallèles déjà formalisés en 2009
  • L’écart principal tient à la vérification des changements d’état séquentiels via un modèle de machine à états, puis à la réutilisation de ce même modèle pour des vérifications de linearisability afin de détecter les race conditions en exécution parallèle
  • Parmi les bibliothèques étudiées, beaucoup n’ont pas de tests stateful ou seulement un support expérimental, et les tests parallèles sont encore plus rares : des issues liées à ce sujet restent ouvertes depuis des années dans FsCheck, Gopter, RapidCheck, SwiftCheck, jsverify, etc.
  • Une implémentation Haskell d’environ 400 lignes reproduit le property-based testing stateful et parallèle, et utilise comme modèle une implémentation de référence basée sur un fake, plus familière aux développeurs qu’une spécification traditionnelle par machine à états
  • Un fake testé par contrat peut être réutilisé au-delà de la validation d’un composant unique, notamment dans des tests d’intégration rapides et déterministes où il remplace des dépendances réelles par injection

Le fossé fonctionnel apparu après QuickCheck

  • Le property-based testing s’est propagé dans plusieurs communautés de programmation sous le slogan « n’écrivez pas des tests, générez-les »
  • La page Wikipédia de QuickCheck, la bibliothèque Haskell d’origine, recense 57 réimplémentations dans d’autres langages
  • Le premier article sur QuickCheck, QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs, a été présenté à l’ICFP 2000, et le code source complet de la première implémentation tenait dans environ 300 lignes en annexe de l’article
  • Le QuickCheck initial ne pouvait tester que des fonctions pures, puis Testing monadic code with QuickCheck (2002) a posé les bases pour traiter du code à effets comme l’état mutable, les E/S fichier ou le réseau

L’apparition des tests stateful et parallèles

  • Quviq AB a été fondée en 2006 par John Hughes et Thomas Arts, avec comme cas d’usage initial les tests du projet Erlang chez Ericsson
  • Erlang n’est pas un langage purement fonctionnel et la concurrence y est courante, ce qui rendait le QuickCheck monadique existant insuffisamment pratique à lui seul
  • Le QuickCheck Erlang propriétaire de Quviq incluait ensuite deux fonctionnalités absentes de nombreuses implémentations open source
    • le property-based testing stateful séquentiel à l’aide de modèles de machines à états
    • des tests parallèles réutilisant ce même modèle de machine à états séquentiel pour détecter des race conditions
  • Les tests stateful apparaissent sous leur forme actuelle dans QuickCheck testing for fun and profit (2007)
  • Les tests parallèles sont détaillés dans Finding Race Conditions in Erlang with QuickCheck and PULSE (ICFP 2009), qui s’appuie comme technique centrale sur Linearizability: a correctness condition for concurrent objects (1990) de Herlihy et Wing
  • Le code de la bibliothèque Quviq QuickCheck n’a pas été partagé dans les articles ; seuls l’API et des exemples de tests utilisant cette API étaient publics

Résultats de l’étude des bibliothèques en 2024

  • L’état de l’art actuel repose sur les tests stateful fondés sur des modèles de machines à états, et sur les tests parallèles combinant ce même modèle séquentiel avec la linearisability
  • L’étude synthétise des lectures de documentation, d’issue trackers et d’une partie du code source, arrêtées à juillet 2024
  • De nombreuses bibliothèques ne proposent pas de tests stateful, ou seulement de manière limitée
    • QuickCheck (Haskell) a une issue ouverte depuis 2016 sur l’ajout des tests stateful
    • SwiftCheck a également une issue ouverte depuis 2016 sur l’ajout des tests stateful
    • jsverify conserve depuis 2015 une issue sur l’ajout des tests stateful
    • proptest (Rust) renvoie vers un projet séparé, proptest-state-machine
  • Le support des tests parallèles est encore plus rare
    • Gopter indique dans son README « No parallel commands … yet? » et a une issue ouverte depuis 2017
    • FsCheck a une issue ouverte depuis 2016 sur l’ajout du support parallèle
    • RapidCheck a une issue ouverte depuis 2015 sur l’ajout du support parallèle
    • propcheck a une issue ouverte depuis 2020 sur l’ajout des tests parallèles
  • Parmi les exemples open source prenant en charge les deux fonctionnalités figurent PropEr, Hedgehog, qcheck-stm, quickcheck-state-machine et stateful-check
  • Même lorsqu’une fonction parallèle existe, elle peut être limitée
    • Dans QuickTheories, un commentaire du code source indique que les tests parallèles doivent en général limiter la command list à 10 éléments ou moins, car le nombre d’end states possibles augmente rapidement avec le nombre de commandes
    • Les exemples LevelDB et Redis de ScalaCheck sont présentés comme des exemples séquentiels avec threadCount = 1
    • Le support des race conditions dans fast-check ne semble pas, contrairement aux tests parallèles de Quviq QuickCheck, réutiliser un modèle de machine à états séquentiel ni employer la linearisability
  • Il n’existe pas d’exemple clair où les tests parallèles auraient été ajoutés plus tard sans difficulté ; s’ils ne sont pas prévus dès la conception de l’API, ils peuvent exiger une refonte importante

Pourquoi la diffusion de ces fonctionnalités a été lente

  • John Hughes avance trois explications
    • les tests stateful et parallèles sont moins utiles que les tests de fonctions pures
    • écrire des modèles de machines à états demande une manière de penser différente des tests classiques et nécessite de la formation
    • l’open source seul favorisait mal l’adoption industrielle, tandis qu’un produit closed source accompagné de formation et de conseil l’a facilitée
  • Tester uniquement des fragments de fonctions pures avec le property-based testing apporte déjà beaucoup, mais les systèmes industriels contiennent aussi des bases de données, des protocoles stateful et des structures de données concurrentes ; les tests stateful et parallèles sont donc presque aussi importants
  • Une spécification stateful n’est pas toujours plus difficile qu’une spécification de fonction pure
    • un modèle de magasin clé-valeur peut déjà aller très loin avec une simple liste de paires clé-valeur
    • dans le cas de LevelDB, un modèle simple a trouvé en quelques minutes un contre-exemple réduit de 17 étapes, puis après un correctif de Google un autre contre-exemple de 31 étapes en quelques minutes encore
    • le second problème venait d’un bug dans le background compaction process ; la compaction est importante pour améliorer les performances de lecture et récupérer de l’espace disque, mais elle n’était pas explicitement incluse dans le modèle
  • Le closed source a peut-être aidé l’adoption dans l’industrie, mais n’a pas aidé l’adoption open source selon cette analyse
  • Reproduire les résultats des articles sans licence Quviq QuickCheck demanderait tellement de reverse engineering que cela serait presque impossible

Proposition : une implémentation petite, ouverte et des spécifications plus simples

  • Deux pistes d’amélioration sont proposées
    • fournir une implémentation open source courte du property-based testing stateful et parallèle, à l’image des quelque 300 lignes du QuickCheck d’origine
    • réduire la charge d’écriture des spécifications en réutilisant, à la place des machines à états, des concepts déjà familiers aux développeurs comme les mocks et les test doubles
  • Pour vérifier cette hypothèse, deux démonstrations sont proposées
    • une implémentation du property-based testing stateful et parallèle en environ 400 lignes de code
    • l’utilisation, à la place d’une state machine, d’une implémentation de référence en mémoire, autrement dit un fake, comme modèle

Résumé des tests purement property-based

  • Dans les tests de fonctions pures, on génère des entrées et on vérifie que la sortie de la fonction satisfait une certaine relation avec l’entrée
  • Par exemple, reverse peut être testé avec la propriété reverse (reverse xs) == xs pour une liste arbitraire xs
  • QuickCheck génère par défaut 100 tests et, en cas d’échec, réduit l’entrée pour présenter le plus petit contre-exemple possible
  • Une propriété erronée comme reverse xs == xs est réduite à un contre-exemple minimal comme [0,1]
  • Les motifs de propriétés les plus fréquents sont l’inverse, l’idempotence, l’associativité, les axiomes des types de données abstraits, les propriétés métamorphiques, etc.
    • inverse : deserialise (serialise i) == i
    • idempotence : sort (sort xs) == sort xs
    • associativité : (i + j) + k == i + (j + k)

Tests property-based à état

  • Les composants avec état ne produisent pas toujours la même sortie pour la même entrée
    • le résultat du premier incr d’un compteur et celui du deuxième incr dépendent de l’état précédent
    • les bases de données et les systèmes de fichiers sont eux aussi influencés, pour leurs sorties futures, par l’historique des entrées précédentes
  • Si les tests de fonctions pures manipulent une entrée unique, les tests à état génèrent des séquences d’entrées pour vérifier comment le système évolue dans le temps
  • Le modèle est représenté par un faux composant de forme m -> i -> (m, o)
    • à partir de l’état de modèle précédent m et de l’entrée i, on calcule le modèle suivant et la sortie o
    • on compare à chaque étape la sortie du système réel à celle du faux composant
    • en cas d’écart, on réduit la séquence d’entrées pour trouver un petit contre-exemple

  • Exemple de compteur

    • on prend comme cible de test un compteur Haskell utilisant une variable mutable globale
    • incr incrémente le compteur et get lit la valeur actuelle
    • un seul Counter Int suffit comme modèle, et l’instance StateModel définit l’état initial Counter 0, Incr, Get, Incr_ (), Get_ Int, runFake, runReal et le générateur de commandes
    • si l’on introduit un bug comme incr42Bug, où le compteur n’augmente pas quand sa valeur est 42, QuickCheck trouve un échec après 66 tests, effectue 29 réductions et présente comme contre-exemple minimal un Get après 43 incréments
    • si l’on ne fait pas reset du compteur global réel entre les tests, le modèle démarre toujours à 0 mais le compteur réel conserve l’état du test précédent, ce qui provoque un décalage

  • Interface des bibliothèques à état

    • l’interface StateModel considère le système sous test comme une black box, avec les commandes en entrée et les réponses en sortie
    • ses éléments centraux sont Command state, Response state, initialState, runFake, runReal, generateCommand
    • les éléments optionnels sont les suivants
      • Reference : utilisé quand une ressource créée par une réponse précédente, comme un file handle, est référencée dans une commande ultérieure
      • PreconditionFailure : représente un échec de précondition, par exemple lorsqu’on empêche une lecture depuis un handle qui ne correspond pas à un fichier ouvert
      • CommandMonad : IO par défaut, mais d’autres monades peuvent être utilisées
      • monitoring, commandName : utilisés pour la couverture et les statistiques
    • lors de la génération des commandes, on ne peut pas créer de vraies valeurs comme un file handle réel ; on génère donc des références symboliques de forme Var Int, remplacées par les références réelles pendant l’exécution
    • après réduction, on supprime les commandes qui violent les préconditions ou utilisent des références symboliques hors de leur portée

  • Exemple de buffer circulaire

    • on teste via la FFI Haskell une file circulaire écrite en C, avec comme modèle une simple file basée sur une liste
    • l’implémentation C ne fait pas de vérification d’erreur ; appeler get sur une file vide peut donc renvoyer une zone mémoire non initialisée
    • l’implémentation réelle est efficace grâce à des index circulaires, mais n’est pas manifestement correcte, tandis que le faux modèle est moins efficace mais cela n’a pas d’importance pour les tests
    • comme new renvoie une référence de file, le modèle gère plusieurs files via Map (Var Queue) FQueue
    • au départ, la précondition interdisant put sur une file pleine manquait ; quand on mettait 0, puis 1 dans une file de taille 1 avant d’appeler get, le modèle attendait 0 selon l’ordre FIFO, mais le code C renvoyait 1
    • ce n’était pas un bug d’implémentation mais un oubli de précondition dans le modèle, corrigé en ajoutant la précondition QueueIsFull
    • l’absence de la commande Size dans le générateur a été révélée par la sortie de couverture ; une fois ajoutée, elle a permis de découvrir un bug dans le calcul de la taille de la file
    • si l’on met un élément dans une file de taille 1 puis qu’on appelle Size, la valeur attendue est 1 mais la valeur réelle est 0 ; une correction proposée consiste à définir la taille du buffer interne à n + 1 dans new
    • ensuite, abs(q->inp - q->outp) % q->size passe pour la taille 1 mais échoue à nouveau pour la taille 2, et la correction finale est (q->inp - q->outp + q->size) % q->size

  • L’énigme des cruches de Die Hard 3

    • l’énigme consistant à obtenir exactement 4 L avec des cruches de 3 L et 5 L est résolue avec des tests à état
    • même sans implémentation réelle, exécuter uniquement le modèle et le faux composant permet de faire échouer le test quand un état donné est atteint, afin d’obtenir une séquence d’actions réduite
    • après 199 tests et 11 réductions, la séquence proposée suit le déroulé suivant
      • remplir la cruche de 5 L
      • verser de la cruche de 5 L dans celle de 3 L
      • vider la cruche de 3 L
      • verser à nouveau de la cruche de 5 L dans celle de 3 L
      • remplir la cruche de 5 L
      • verser de la cruche de 5 L dans celle de 3 L
    • la trace affiche les états intermédiaires, ce qui permet de vérifier comment la grande cruche atteint 4 L

Tests property-based en parallèle

  • les bugs du code concurrent sont difficiles à reproduire et à valider lors du correctif, car l’interleaving des threads change à chaque exécution
  • l’objectif est de permettre aux utilisateurs d’effectuer des tests en parallèle, comme avec des tests séquentiels basés sur l’état, sans avoir à écrire beaucoup de code de test supplémentaire
  • dans l’exemple du compteur, si incr effectue readIORef puis writeIORef de manière non atomique, deux threads peuvent écraser mutuellement leur incrément, ce qui provoque une race condition
  • le test en parallèle collecte les instants d’invocation et de réponse des commandes pendant l’exécution pour construire un historique concurrent, puis vérifie si cet historique peut s’expliquer par un interleaving séquentiel
  • si au moins un interleaving est compatible avec le modèle séquentiel, l’historique est considéré comme linéarisable et donc correct
  • si aucun interleaving séquentiel ne permet d’expliquer les réponses observées, le résultat est traité comme non linéarisable

  • Génération et shrink des commandes parallèles

    • un programme parallèle est représenté par ParallelCommands et plusieurs Fork, les commandes à l’intérieur de chaque Fork étant exécutées en parallèle
    • l’implémentation d’exemple traite des exécutions mono-, bi- et tri-thread
    • en exécution parallèle, comme avec Fork [Write "a" "foo", Write "a" "bar"], les états possibles du modèle peuvent varier selon l’interleaving
    • le modèle parallèle effectue la génération et le shrink des commandes non pas à partir d’un état unique, mais d’un ensemble d’états
    • parallelSafe vérifie que la précondition reste satisfaite pour toutes les permutations des commandes dans un Fork
    • par exemple, si Write "a" et Delete "a" se trouvent dans le même fork, une commande peut invalider la précondition de l’autre
    • lors du shrink, seules sont conservées les commandes qui préservent la précondition et la portée des références symboliques

  • Exécution parallèle et vérification de la linéarisabilité

    • l’exécution parallèle enregistre les événements Invoke et Ok de chaque commande dans l’historique
    • si une réponse contient une nouvelle référence, l’environnement est étendu avec un compteur atomique afin d’éviter les collisions de numéros de référence entre threads
    • tous les interleavings possibles de l’historique sont énumérés sous forme d’arbre Rose
    • linearisable vérifie si un chemin quelconque de cet arbre fait correspondre les réponses observées avec le modèle séquentiel runFake
    • comme les tests parallèles réutilisent finalement le modèle séquentiel, l’utilisateur obtient des tests parallèles avec peu de code supplémentaire après avoir écrit le modèle séquentiel

  • Exemple de compteur parallèle

    • pour activer le test parallèle du compteur, le seul code supplémentaire ajouté est l’instance ParallelModel Counter et la property
    • avec incrRaceCondition non atomique, une race condition est détectée
    • même si une race existe aussi dans un test case plus petit, si l’échec ne se reproduit pas à cause d’un interleaving différent, QuickCheck peut considérer que ce test plus petit passe et arrêter le shrink
    • la bonne solution est d’utiliser un ordonnanceur de threads déterministe, ce qu’emploie l’article sur les tests parallèles
    • l’implémentation d’exemple utilise à la place un workaround plus simple consistant à insérer un court sleep autour des lectures/écritures en mémoire partagée afin d’augmenter la probabilité de reproduire le même interleaving
    • ce sleep n’est pas nécessaire pour trouver la race, mais pour réduire le contre-exemple trouvé à une forme plus petite
    • après l’ajout du sleep, le contre-exemple minimal se réduit à ParallelCommands [Fork [Incr,Incr],Fork [Get]]

  • Exemple de registre de processus

    • on utilise comme exemple un système, semblable au registre de processus d’Erlang, qui spawn des threads et enregistre, recherche, désenregistre et kill des ThreadId par nom
    • le modèle séquentiel suit les identifiants de thread créés, les paires nom-thread enregistrées et les identifiants de thread killés
    • Register et Unregister peuvent échouer, la réponse utilise donc Either ErrorCall ()
    • dans l’implémentation réelle, les informations de localisation des erreurs sont supprimées via abstractError pour correspondre au fake
    • monitoring affiche la couverture RegisterFailed, RegisterSucceeded, UnregisterFailed, UnregisterSucceeded
    • si l’on introduit volontairement un bug où register écrase le registre existant, on obtient un contre-exemple séquentiel où il est impossible de désenregistrer "e" pourtant déjà enregistré
    • en test parallèle, un contre-exemple plus long apparaît et, avec SleepyIORef, il est réduit à une forme comme Fork [Register "b" (Var 0), Register "c" (Var 0)]
    • le problème est une race où un autre thread peut s’intercaler entre la vérification via readRegistry et l’appel à atomicModifyIORef
    • après application d’un verrou global à register, unregister et kill, les tests parallèles passent

Modèles basés sur des fake et tests d’intégration

  • Au lieu d’une specification traditionnelle de machine à états avec post-conditions, on utilise un fake en mémoire comme implémentation de référence
  • L’article de 2019 d’Edsko de Vries, article de 2019, est présenté comme le premier à proposer une implémentation de fake au-dessus d’une spécification de machine à états fondée sur les post-conditions
  • Le fake est présenté comme une approche plus accessible pour les programmeurs peu familiers des spécifications formelles, un peu à la manière d’un mock
  • Le fake a aussi l’avantage de pouvoir remplacer des composants dépendants dans les tests d’intégration
    • Il n’est pas nécessaire de démarrer ou d’activer la vraie dependency
    • Cela permet de construire des tests d’intégration plus rapides et déterministes
  • Le fait qu’un fake puisse être incorrect est traité par des contract tests
  • Comme les tests property-based parallèles et fondés sur l’état vérifient la correspondance entre le fake et l’implémentation réelle, le fake joue le rôle d’une dépendance testée par contrat

  • Séparer tests et déploiement avec un fake de queue

    • L’interface de queue IQueue expose iNew, iPut, iGet, iSize
    • L’implémentation réelle connecte directement un wrapper de queue en C
    • L’implémentation fake stocke l’état du modèle dans IORef et le met à jour via fNew, fPut, fGet, fSize
    • Le composant est écrit contre l’interface IQueue q
    • En test, on utilise une instance fake, et en déploiement une instance real
    • On pose l’hypothèse qu’avec des tests property-based fondés sur l’état, le fake est fidèle au real

  • Fake de système de fichiers

    • L’interface de système de fichiers IFileSystem h expose iMkDir, iOpen, iWrite, iClose, iRead
    • L’implémentation réelle utilise le vrai système de fichiers sous /tmp/qc-test
    • Le fake est implémenté comme un FakeFS en mémoire avec un ensemble de répertoires, une map du contenu des fichiers, une map des handles ouverts et le prochain handle
    • fOpen, fWrite, fClose, fRead modélisent les échecs de précondition comme un fichier occupé, un répertoire inexistant ou un handle fermé
    • Si le fake du système de fichiers est testé et jugé fidèle au vrai système de fichiers, les composants qui en dépendent peuvent être testés en intégration avec le fake puis remplacés en déploiement par le vrai système de fichiers
    • Si un bug apparaît après remplacement par le réel, il faut examiner comment un décalage entre fake et real a pu passer les tests property-based fondés sur l’état

  • Systèmes de composants plus vastes

    • La même approche s’étend à des systèmes où A dépend de B et B dépend de C
    • On définit une interface pour chaque composant
      • iC :: IO IC
      • iB :: IC -> IO IB
      • iA :: IB -> IO IA
    • La stratégie de test est la suivante
      • On valide C avec des tests property-based parallèles et fondés sur l’état afin d’obtenir un fake C testé par contrat
      • Dans les tests d’intégration de B, on utilise le fake C
      • Pour tester A, on utilise un fake B qui lui-même utilise le fake C
    • Cette approche se généralise au même pattern pour davantage de composants ou de services

Conclusion

  • Les tests property-based parallèles et fondés sur l’état peuvent être implémentés en environ 400 lignes de code, une taille comparable à la première implémentation de QuickCheck, qui comptait environ 300 lignes sans shrinking
  • Utiliser un fake comme modèle donne aux tests parallèles et fondés sur l’état une forme de spécification plus familière, et permet de les réutiliser pour tester de plus grands systèmes de manière compositionnelle
  • Si chaque communauté de langage poursuit ses expérimentations, il existe une marge d’amélioration pour l’état des bibliothèques de tests property-based

À lire aussi

1 commentaires

 
GN⁺ 2024-07-06
Avis de Hacker News

  • Avec l’arrivée du fuzzing guidé par la couverture, et son bon support dans Go, je me demande ce qu’on rate si l’on n’utilise pas de bibliothèque de tests basés sur les propriétés
    https://www.tedinski.com/2018/12/11/fuzzing-and-property-tes...
    En regardant le test de fuzzing ci-dessous et la vérification d’invariant correspondante, j’ai l’impression que c’est en pratique presque la même chose qu’un test de propriété
    https://github.com/ncruces/aa/blob/505cbbf94973042cc7af4d6be...
    https://github.com/ncruces/aa/blob/505cbbf94973042cc7af4d6be...

    • La distinction entre tests basés sur les propriétés et fuzzing relève surtout d’un regroupement assez grossier, une question d’ambiance
      Il existe de vraies différences, mais la frontière est assez floue, et il n’est pas si important de déterminer précisément ce qui relève du fuzzing ou des tests basés sur les propriétés
      Les tests rapides avec des assertions détaillées relèvent des tests basés sur les propriétés ; ceux qui tournent longtemps et ne cherchent que des crashs relèvent du fuzzing ; entre les deux, c’est ambigu
      https://hypothesis.works/articles/what-is-property-based-tes...
    • Le fuzzing guidé par la couverture et les tests basés sur les propriétés peuvent tout à fait être combinés
      Quand j’étais chez Google, un outil interne qui combinait les deux était vraiment excellent. On écrivait un test basé sur les propriétés comme d’habitude, puis à l’exécution le framework de test compilait spécialement le code pour obtenir la couverture et ajustait les entrées aléatoires afin de l’augmenter. Bien sûr, tout cela tournait de façon entièrement automatique sur un cluster de plusieurs machines
      Les tests basés sur les propriétés traditionnels sont généralement implémentés uniquement sous forme de bibliothèque, donc ils ne disposent pas forcément d’informations de couverture pour guider la génération des entrées aléatoires
    • Puisque des propriétés sont assertées, je considérerais que cela relève, par définition, des tests basés sur les propriétés, par exemple « tous les nœuds dont le niveau est supérieur à 1 ont deux enfants »
      Cela dit, selon la bibliothèque, on peut bénéficier de pas mal de fonctionnalités pratiques. L’une des choses utiles est le shrinking ; voir la section « Shrinking » ici : https://tech.fpcomplete.com/blog/quickcheck-hedgehog-validit...
      Les combinateurs permettant de composer des générateurs sont aussi excellents, et certaines bibliothèques disposent d’un ensemble de valeurs « mauvaises » connues pour déclencher des comportements exceptionnels
    • Je ne sais pas très bien en quoi les tests de fuzzing de Go diffèrent de ce que dit l’article lié, mais celui-ci affirme qu’un vrai fuzzer doit tourner pendant des jours ou des semaines, et qu’il faut presque toujours choisir les tests basés sur les propriétés plutôt que le fuzzing
      J’aimerais prendre un peu de recul et poser une question plus méta sur les tests. Est-ce qu’un test réussi signifie que le code est correct, et inversement ? Y a-t-il dans le contrat de Go un passage indiquant que fournir la même entrée au même code produit la même sortie ?
    • Du point de vue de l’API, ce qu’on obtient surtout, c’est une bibliothèque de combinateurs pour générer les structures de données aléatoires que l’on veut
      En manipulant le type Arbitrary, qui représente un ensemble d’objets aléatoires, on peut facilement écrire des fonctions réutilisables pour générer des entrées de test. Ce genre de bibliothèque pourrait probablement être utilisé assez facilement avec le framework de fuzzing de Go
      Cela dit, je trouve que les combinateurs classiques comme map, filter, chain ou oneOf peuvent être un peu maladroits, donc je travaille sur une nouvelle bibliothèque de tests de propriétés pour JavaScript. L’objectif est de la rendre plus agréable à utiliser, mais elle est encore expérimentale et pas encore publique

  • clojure.spec.alpha offrait une excellente expérience, qu’on l’utilise ou non avec test.check, mais après avoir essayé hypothesis en Python, j’ai trouvé ça vraiment médiocre
    Hypothesis semblait incapable, par conception, de gérer des jeux de données simples mais « gros », et ici « gros » ne veut en fait pas dire si gros que ça. [0] C’était tellement pénible que nous avons carrément retiré Hypothesis et les tests fondés sur la génération de la suite de tests Python au travail
    [0] https://github.com/HypothesisWorks/hypothesis/issues/3493

    • Dans ce cas, on dirait moins qu’Hypothesis ne sait pas gérer les grands jeux de données que le fait qu’il rejetait une grande partie des cas réduits
      Hypothesis essayait de réduire les entiers générés à 0 pour voir si le bug existait aussi à 0, et le test rejetait le cas, au lieu d’échouer, parce qu’il contenait 0. Sur de petits cas, cela se limitait à une inefficacité, mais sur de grands cas, c’en était au point qu’Hypothesis abandonnait
      Dans ce fil, quelqu’un a suggéré d’utiliser une autre stratégie de génération d’instances, qui ne puisse pas produire de 0. Autrement dit, ne pas générer la valeur préférée du réducteur d’Hypothesis pour ensuite la rejeter, mais éviter de la produire dès le départ. Je me demande si cela a été essayé
      Je me demande aussi en quoi clojure.spec.alpha gère cela différemment
      Le commentaire de mjaniczek sur https://news.ycombinator.com/item?id=40876437 cite ce cas comme un inconvénient de l’approche d’Hypothesis
      L’idée est que « le générateur devient maintenant un parseur de liste d’octets susceptible d’échouer, ce qui introduit une certaine inefficacité, et l’utilisateur peut créer des générateurs étranges que le réducteur interne ne parvient pas à réduire parfaitement. Malgré tout, l’expérience développeur est la meilleure des trois approches… »
      Bien sûr, la personne n’accepterait probablement pas l’idée d’avoir écrit son test d’une façon « étrange »
    • J’aimais le fait que le spec de Clojure soit vraiment facile à structurer autour de soi, mais après être passé à Elixir, il fallait descendre jusqu’à propEr, une vieille bibliothèque Erlang, pour écrire ce genre de tests. Assez décevant
    • L’exemple dans l’issue GitHub utilise filter d’une manière qui provoque son propre problème
      Si l’on génère aléatoirement puis que l’on filtre ce qui correspond à une certaine propriété, le processus de génération revient en pratique à gratter un ticket de loterie

  • La réponse simple à la question posée dans l’article — « pourquoi n’exige-t-on pas que les recherches publiées soient reproductibles avec des outils open source, ou au moins avec des outils mis gratuitement à disposition du public et des autres chercheurs ? » — est que la conséquence immédiate d’une telle exigence serait que les articles ne satisfaisant pas cette condition ne seraient pas publiés
    Par exemple, même des travaux comme l’article sur Quviq QuickCheck, qui semblent avoir été utiles aux auteurs et à d’autres personnes, n’auraient pas été publiés, et la communauté aurait perdu ce cadeau qu’est cette information

    • Ce serait bien que certains éditeurs exigent la reproductibilité, et d’autres non
      Toute exigence a un effet d’exclusion, et il y aura toujours des cas limites d’articles qui peuvent être utiles même sans satisfaire une exigence donnée
    • Ce n’est pas une question tranchée, et on pourrait même la qualifier de politique, mais cet argument de défense n’est pas très convaincant pour autant
      Si l’on considère cet argument comme valide, on peut s’en servir comme bouclier pour aller aussi loin qu’on veut. Si l’on abandonne la reproductibilité comme exigence, on n’a plus besoin d’expliquer quoi que ce soit que l’on ne souhaite pas expliquer. Pas besoin de fournir les données sur les échantillons, ni les tests de significativité statistique. Un résumé vague affirmant avoir atteint tel ou tel résultat devient suffisant
      Même la célèbre note laissée par Fermat dans la marge de son exemplaire personnel de l’Arithmetica deviendrait alors un article de recherche pleinement valide. Après tout, on ne voudrait pas perdre l’information précieuse selon laquelle un mathématicien célèbre pensait disposer d’une preuve concise et élégante d’un théorème. Même si, bien sûr, il est très probable qu’elle n’existait pas réellement
      Mon avis sur cette question politique est que les critères actuels sont trop laxistes. Personne n’est contraint de publier quoi que ce soit. Il existe dans le monde beaucoup de recherches qui ne sont publiées nulle part, par exemple pour des raisons de valeur propriétaire, et elles ne vont pas disparaître
      Mais si l’on travaille dans le monde académique, a fortiori avec des financements de recherche, et que l’on affirme avoir pour objectif de faire progresser la connaissance scientifique mondiale, il est juste d’exiger que l’on poursuive réellement cet objectif. Il ne faudrait pas se contenter de faire semblant de le poursuivre pour gravir les échelons d’une carrière universitaire
    • On pourrait aussi imaginer de rendre le code source accessible uniquement aux évaluateurs
      Avec tout ce qui est nécessaire pour exécuter le code. C’est peut-être même déjà ce qui se fait
    • Parce que la reproductibilité est une pierre angulaire de la méthode scientifique
    • Les articles sont publiés parce que leurs auteurs veulent augmenter leur « indice d’importance », qui est très directement lié à la rémunération et aux perspectives de carrière académique
      Ajouter davantage d’exigences à cette fin a peu de chances de réduire le nombre d’articles publiés
      Le problème le plus grave des articles publiés est que, pour publier le plus possible et le plus vite possible, on ferme souvent délibérément les yeux sur les erreurs. Rendre la vérification des articles plus facile pourrait améliorer la situation, mais je n’en attendrais pas trop. Les gens sont très doués pour trouver des raccourcis

  • Avec proptest en Rust, j’écris assez souvent des tests de propriétés avec état, et en général les coder soi-même est assez simple
    Un exemple non trivial ayant trouvé 6 bugs se trouve ici : https://github.com/sunshowers-code/buf-list/blob/main/src/cu...
    Les tests parallèles peuvent parfois être utiles, mais il est souvent plus simple de lancer beaucoup de tests en parallèle

    • En Rust, j’écris beaucoup de tests de propriétés manuels, qui ressemblent généralement à ceci
      Au niveau supérieur, j’utilise une vraie part d’aléatoire, puis plusieurs boucles imbriquées en dessous pour passer de cas de faible complexité à des cas de plus forte complexité. Ensuite, je crée une graine à fournir à un générateur pseudo-aléatoire déterministe et je l’affiche. Si le test échoue, il suffit de copier-coller la graine en erreur pour reproduire le cas d’échec
      J’ai trouvé que ces tests de propriétés manuels étaient plus rapides, plus flexibles et globalement moins pénibles que n’importe quel framework ou bibliothèque
      Cela dit, pour des tests de concurrence vraiment robustes, je recommande vivement la bibliothèque AWS Shuttle (https://github.com/awslabs/shuttle). Elle peut débusquer des conditions de concurrence d’une complexité difficile à croire. J’ai aussi écrit un petit tutoriel : https://grantslatton.com/shuttle
      Chez AWS, cette bibliothèque a été utilisée pour valider un système de fichiers sur mesure écrit pour faire tourner AWS S3

  • J’ai parcouru rapidement l’article lié, “Testing Telecoms Software with Quviq QuickCheck”, mais je n’ai pas vu de réponse immédiate à la question : « pourquoi ne vaudrait-il pas mieux construire soi-même cette opération avec état ? »
    Le texte original renvoie à cette partie avec le modèle de paires clé-valeur d’un magasin clé-valeur, mais je ne vois pas pourquoi on ne pourrait pas simplement écrire une machine à états, ni pourquoi un framework serait nécessaire. La semaine dernière au travail, pour tester des interactions avec un système de fichiers, j’ai littéralement fait cela, et ça s’est finalement résumé à quelque chose comme type Instruction = | Read of stuff | Write of stuff | Seek of stuff | …
    La propriété devient alors : « étant donnée cette liste de commandes, … ». Le type StateModel demande en gros de faire la même chose. J’ai du mal à voir StateModel faire vraiment sa part du travail ; il semble seulement supprimer, d’après mon expérience, une très petite quantité de code de test, au prix de beaucoup plus de code de framework à comprendre

    • Ce jugement est valable pour certains tests, mais la partie réduction des cas d’échec est souvent délicate
      Si l’on veut générer uniquement des séquences de transitions d’état « valides », il faut généralement un état de modèle qui détermine quelles étapes de test sont valides dans un état donné. Il faut aussi éviter que, pendant la réduction, la suppression d’étapes de test casse les préconditions respectées lors de la génération initiale de chaque étape, ce qui produirait de faux échecs
      Si l’on veut simplement des séquences d’opérations arbitraires entièrement aléatoires, où n’importe quelle opération est valide dans n’importe quel état, un framework proptest avec état peut être excessif. Mais si l’on doit maintenir un état de modèle et préciser les préconditions de plusieurs opérations, un framework dédié enlève beaucoup de travail
      J’ai écrit l’an dernier un billet de blog sur ce sujet, qui peut servir de référence si l’on veut un exemple plus approfondi : https://readyset.io/blog/stateful-property-testing-in-rust
      Comme d’autres l’ont dit, les tests de machines à états parallèles sont aussi un avantage intéressant que l’on peut obtenir avec un framework dédié, mais ce n’est pas le seul
    • Je pense que la partie avec état est mieux couverte par les tests basés sur un modèle
      On peut mélanger les styles de test. C’est votre code, après tout
    • Si je comprends bien, QuickCheck parallèle vérifie que tous les entrelacements possibles dans un programme multithread produisent au final un état qui serait aussi atteignable en appelant les commandes séquentiellement
      C’est là son avantage

  • L’auteur se concentre sur les aspects machine à états et parallélisme des tests fondés sur des propriétés, mais il existe aussi d’autres aspects qui pourraient avoir un effet plus important.
    L’un d’eux est le test fondé sur des propriétés guidé par la couverture ; voir l’article de Dan Luu : https://danluu.com/testing/
    Un autre, qui est celui pour lequel j’ai un biais, consiste à automatiser la réduction tout en conservant toutes les invariants créés lors de la génération des valeurs.
    En résumé, les fonctions de réduction dérivées à la QuickCheck qui opèrent sur des valeurs (shrink : a -> [a]) ont des contraintes et des problèmes, au point que les gens finissent par désactiver la réduction plutôt que de traiter le problème.
    La « réduction intégrée » par rosiers (par exemple Hedgehog) respecte les contraintes du générateur, mais pose problème avec le bind monadique, c’est-à-dire lorsque le résultat d’un générateur est utilisé pour bifurquer vers un autre générateur.
    La seule approche qui semble magiquement « juste fonctionner » est la réduction interne de Hypothesis. Elle utilise un niveau d’indirection qui réduit une liste de choix aléatoires plutôt que la valeur elle-même. L’inconvénient est que le générateur devient alors un parseur de liste d’octets susceptible d’échouer, ce qui introduit une certaine inefficacité, et que l’utilisateur peut créer des générateurs étranges que le réducteur interne ne parvient pas à réduire parfaitement. Malgré tout, parmi les trois approches, c’est celle qui offre la meilleure expérience développeur, et si l’on considère que le simple fait que les gens écrivent des tests est déjà un petit miracle, c’est celle qui semble la plus intéressante à construire en tant qu’auteur de bibliothèque de test.

    • Sur le fait que la « réduction intégrée » par rosiers (par exemple Hedgehog) respecte les contraintes du générateur mais a des problèmes avec le bind monadique, dans les limites de mes connaissances d’amateur, je vois cela comme une limite fondamentale du bind monadique / générateur.
      À la place, il faut privilégier les générateurs applicatifs pour une réduction optimale : https://github.com/hedgehogqa/haskell-hedgehog/issues/473#is...
      Autrement dit, les générateurs applicatifs ne « se servent pas du résultat d’un générateur pour bifurquer vers un autre générateur », et la nature « parallèle » de l’applicatif optimise la réduction. Ici, parallèle n’est pas à comprendre au sens des threads de l’article, mais au sens monadique. Comme l’applicatif est « parallèle », les générateurs peuvent être réduits indépendamment. À l’inverse, un générateur monadique est « sériel » : en réduire un change nécessairement le comportement des générateurs qui suivent.
      S’il existe une présentation publique, j’aimerais beaucoup avoir le lien.
    • Personnellement, Hypothesis a été très loin de « juste fonctionner ».
      Je ne pense pas qu’il soit réellement prêt pour la production, et cela semble même être ainsi par conception.[0]
      Ayant pas mal utilisé clojure.spec.alpha, avec ou sans test.check, je n’étais pas complètement étranger à l’idée générale, même s’il y a des différences.
      [0] https://github.com/HypothesisWorks/hypothesis/issues/3493
    • Mon framework préféré est falsify, qui fournit une « réduction intégrée interne ».
      Il est similaire à Hypothesis, mais utilise un arbre de génération plutôt qu’une séquence linéaire. Il repose sur les foncteurs sélectifs, qui constituent aussi une bonne interface utile pour des choses comme les validateurs.
      D’après https://hackage.haskell.org/package/falsify, cette bibliothèque fournit des tests fondés sur des propriétés avec prise en charge de la réduction intégrée interne. Intégrée au sens de Hedgehog, c’est-à-dire qu’il n’est pas nécessaire d’écrire séparément un réducteur et un générateur ; interne au sens de Hypothesis, c’est-à-dire qu’elle fonctionne aussi correctement à travers les binds monadiques.

  • J’ai essayé d’utiliser les tests fondés sur des propriétés, mais j’ai toujours eu l’impression d’être entre deux chaises.
    Si je comprends suffisamment bien une propriété pour la tester strictement, je peux généralement la pousser dans le système de types afin qu’elle soit vraie par construction. Si je veux seulement un simple smoke test, une entrée arbitraire est plus facile.

    • Je me demande quel genre de propriétés tu as en tête.
      Par exemple, on a souvent deux implémentations, l’une naïve, lente mais simple, et l’autre optimisée, et l’on peut comparer leurs sorties sur des entrées arbitraires. C’est une propriété simple et facile à comprendre, mais généralement difficile à intégrer dans le système de types.
      De même, il peut y avoir des propriétés du type « l’ordre dans lequel les entrées sont présentées ne devrait pas importer », ou bien une manière de découper les données telle que max(valeur maximale de A, valeur maximale de B) = maximum(A union B). Comment encoder cela dans le système de types ?
      Ou encore : « pour des A et B arbitraires, une solution optimale trouvée dans A est moins bonne qu’une solution optimale trouvée dans A union B », ou l’idempotence du type f(f(A)) = f(A).
      Toutes ces propriétés sont faciles à comprendre, mais pas faciles à exprimer dans la plupart des systèmes de types.
    • Si c’est possible, faire respecter les contraintes à la compilation est clairement préférable.
      Mais il existe beaucoup de contraintes que les vérificateurs de types grand public ne savent pas gérer. Les types dépendants aideraient beaucoup, mais ils semblent encore cantonnés à des niches comme les assistants de preuve.

  • Je me demande si la version originale QuviQ Erlang QuickCheck ne manque pas dans la liste.
    Le produit complet est propriétaire, mais une version gratuite, QuickCheck Mini, est aussi disponible : http://www.quviq.com/downloads/

  • Clojure dispose désormais lui aussi d’une bibliothèque quickcheck avec état : https://github.com/griffinbank/test.contract
    Les tests parallèles sont intéressants, mais ils n’ont pas encore été une grande source de douleur.

  • Pour les tests C#/.NET, j’utilise CsCheck[0] et j’en suis plutôt satisfait
    Il est bien plus accessible que Hedgehog ou FsCheck, et aussi assez rapide
    [0] https://github.com/AnthonyLloyd/CsCheck