Tester et prouver (Haskell, Idris)

Voir aussi : video youtube - code source

Développer un logiciel ne se résume pas à écrire son code. Il est également important de s’assurer que le code est “correct”. Si les fonctionnalités du langage, le compilateur et des outils d’analyse de code permettent déjà de détecter certaines erreurs, ils ne sont généralement pas suffisants.

Cet article présente succinctement quelques outils pour valider du code : tests unitaires, tests de propriétés, système de preuves.

Tests unitaires (Haskell Hspec)

Les systèmes de tests unitaires sont des outils très classiques, dans de nombreux langages de programmation. Ils permettent de vérifier automatiquement que des appels de fonctions prédéfinis produisent bien les résultats attendus.

Soient, par exemple, les fonctions mylength et myappend suivantes, en Haskell :

mylength :: [a] -> Int
mylength [] = 0
mylength (x:xs) = 1 + mylength xs

myappend :: [a] -> [a] -> [a]
myappend [] ys = ys
myappend (x:xs) ys = x : (myappend xs ys)

Pour tester ces fonctions (avec Hspec), on peut vérifier que mylength retourne bien la valeur 0 si on l’appelle avec le paramètre [], la valeur 9 avec le paramètre [1..9], etc. C’est ce que permettent les tests unitaires :

main :: IO ()
main = hspec $ do

    describe "mylength" $ do
        it "[]" $ mylength [] `shouldBe` 0
        it "[1..9]" $ mylength [1..9] `shouldBe` 9

    describe "myappend" $ do
        it "[] [5..9]" $ myappend [] [5..9] `shouldBe` [5..9]
        it "[1..4] []" $ myappend [1..4] [] `shouldBe` [1..4]
        it "[1..4] [5..9]" $ myappend [1..4] [5..9] `shouldBe` [1..9]

Concrêtement, il s’agit d’un programme qui, pour chaque test implémenté, appelle la fonction sur le paramètre donné et vérifie que la valeur retournée est bien la valeur attendue. Le programme de test se lance comme un programme classique :

$ runghc Test.hs 

mylength
  []
  [1..9]
myappend
  [] [5..9]
  [1..4] []
  [1..4] [5..9]

Finished in 0.0004 seconds
5 examples, 0 failures

L’avantage d’un tel programme de test est d’automatiser les vérifications. De plus, si on modifie le code de base, on peut relancer le programme de test et ainsi détecter une éventuelle régression :

$ runghc Test.hs 

mylength
  []
  [1..9] FAILED [1]
myappend
  [] [5..9]
  [1..4] []
  [1..4] [5..9]

Failures:

  Test.hs:10:23: 
  1) mylength [1..9]
       expected: 9
        but got: 0

  To rerun use: --match "/mylength/[1..9]/"

Randomized with seed 1567467146

Finished in 0.0009 seconds
5 examples, 1 failure

On notera cependant que les tests unitaires ne valident que les fonctions testées et uniquement pour les paramètres donnés. C’est donc à la charge du développeur que d’écrire des tests unitaires assurant une bonne couverture de code (fonctions + valeurs de paramètres).

Tests de propriétés (Haskell QuickCheck)

Les tests de propriétés peuvent être vus comme une généralisation des tests unitaires : on implémente une propriété que doit respecter une fonction et le programme de test va automatiquement générer des valeurs de paramètres, appeler la fonction avec ces paramètres et vérifier que la propriété est bien respectée.

Par exemple pour la fonction myappend, on peut vérifier (avec QuickCheck) que la liste vide est un élément neutre (à gauche et à droite), ou encore que la taille de l’ajout vaut la somme des tailles initiales.

main :: IO ()
main = hspec $ 

    describe "myappend" $ do

        prop "[] ys = ys" $ \ys -> 
            myappend [] ys `shouldBe` (ys::[Int])

        prop "xs [] = xs" $ \xs -> 
            myappend xs [] `shouldBe` (xs::[Int])

        prop "length (myappend xs ys) = length xs + length ys" $ \(xs, ys) -> 
            mylength (myappend xs ys) `shouldBe` mylength xs + mylength (ys::[Int])

Ici, les propriétés sont implémentées par des fonctions et c’est le système de test qui va générer les entrées à lui fournir. Par défaut, le système sélectionne aléatoirement 100 valeurs parmi le domaine correspondant au type de données mais on peut paramétrer plus finement les entrées à tester.

$ runghc Prop.hs 

myappend
  [] ys = ys
    +++ OK, passed 100 tests.
  xs [] = xs
    +++ OK, passed 100 tests.
  length (myappend xs ys) = length xs + length ys
    +++ OK, passed 100 tests.

Finished in 0.0061 seconds
3 examples, 0 failures

Si une entrée invalide une propriété, le système de test essaie de réduire l’entrée à la valeur la plus simple qui invalide la propriété. Ceci permet de simplifier le travail de debug que le développeur devra faire ensuite.

Failures:

  Prop.hs:15:13: 
  1) myappend xs [] = xs
       Falsifiable (after 2 tests and 1 shrink):
         [0]
       expected: [0]
        but got: []

Ainsi les tests de propriétés permettent de vérifier des fonctions un peu plus exhaustivement par rapport à leurs entrées. Cependant, cela reste une vérification sur des entrées ponctuelles, et a posteriori.

Preuves de programmes (Idris)

Les preuves de programmes peuvent être vues comme des preuves, au sens mathématique, vérifiées avant la génération du programme. Il existe différents outils permettant de prouver des programmes, principalement des assistants de preuves et des langages intégrant des fonctionnalités de preuve : Coq, Isabelle, Agda, Idris, ATS, Lean…

Idris est un langage de programmation, inspiré de Haskell, qui permet également d’écrire des preuves. Par exemple, les fonctions mylength et myappend précédentes peuvent s’écrire, en Idris :

mylength : List a -> Nat
mylength [] = 0
mylength (x::xs) = 1 + mylength xs

myappend : List a -> List a -> List a
myappend [] ys = ys
myappend (x::xs) ys = x :: (myappend xs ys)

Idris supporte les types dépendants. Très grossièrement, cela signifie que les notions de valeur et de type ne sont pas aussi distinctes qu’en Haskell. On peut par exemple définir des types qui dépendent de valeurs, écrire des fonctions qui manipulent des types, ou encore appeler des fonctions dans une signature de fonction.

Ainsi, on peut énoncer et prouver des propriétés. Par exemple, on peut écrire la propriété 1 + 1 = 2 et sa démonstration (réflexivité), qui sera vérifiée automatiquement à la compilation :

prop_1_plus_1 : 1 + 1 = 2
prop_1_plus_1 = Refl

Pour écrire des preuves, il est généralement pratique d’interagir avec le système de vérification. Par exemple, si on essaie de prouver la propriété suivante :

prop_radiohead : 2 + 2 = 5
prop_radiohead = Refl

alors le compilateur génère une erreur avec des indications détaillées :

$ idris2 Proof.idr -o Proof && ./build/exec/Proof
Error: While processing right hand side of prop_radiohead. When unifying:
    5 = 5
and:
    2 + 2 = 5
Mismatch between: 5 and 4.

Proof:26:18--26:22
 22 | prop_1_plus_1 : 1 + 1 = 2
 23 | prop_1_plus_1 = Refl
 24 | 
 25 | prop_radiohead : 2 + 2 = 5
 26 | prop_radiohead = Refl
                       ^^^^

On peut ainsi utiliser le système de preuve de Idris pour vérifier notre code, par exemple que la taille d’une liste vide est nulle et que l’insertion d’un élément fait augmenter la taille de 1.

prop_length_nil : mylength [] = 0
prop_length_nil = Refl

prop_length_cons : (x : a) -> (xs : List a) -> mylength (x::xs) = 1 + mylength xs
prop_length_cons x xs = Refl

Ici, les propriétés correspondent à la définition même de la fonction. Généralement les démonstrations sont plus compliquées et les systèmes de preuves fournissent de nombreuses fonctionnalités pour aider à les écrire. Par exemple, la fonction cong permet de vérifier qu’une application de fonction respecte la propriété voulue :

prop_length_append : (xs, ys : List a) -> mylength (myappend xs ys) = mylength xs + mylength ys
prop_length_append [] ys = Refl 
prop_length_append (x::xs) ys = cong S (prop_length_append xs ys)

Ceci n’est qu’un bref aperçu de l’écriture de preuves, qui est un domaine à part entière (pour une introduction plus détaillée, voir par exemple la vidéo : Haskell for Imperative Programmers #41 - Formal Verification (using Isabelle)).

Conclusion

Lorsqu’on développe un logiciel, il est important vérifier que celui-ci produit bien les résultats attendus. Il existe différents outils pour cela. Les tests unitaires permettent de tester le résultat d’appels de fonctions sur des paramètres donnés. Les tests de propriétés permettent de tester sur des paramètres générés automatiquement.

Enfin, les preuves de programmes permettent une vérification formelle, avant même la génération du programme. Mais cela demande un travail significativement plus important, ce qui n’est pas forcément justifié pour tous les projets ou domaines.