Tests ou types

Salut, Habr. L'autre jour, je cherchais comment faire quelque chose dans Idris, et je suis tombé sur un bon article, dont une traduction gratuite semble tout à fait appropriée. Libertés et bâillon, le cas échéant, je désignerai «ici par de tels gribouillis au début et à la fin».

Quand utiliser les tests et quand - types? Quelles informations et quelles garanties recevons-nous en échange de nos efforts pour les rédiger?

Nous examinerons un exemple simple et légèrement artificiel exprimé en Python, C, Haskell et Idris. Nous verrons également ce qui peut être dit sur la mise en œuvre sans aucune connaissance supplémentaire à ce sujet, dans chaque cas.

Nous ne prendrons pas en compte les divers backdoors qui nous permettent de violer explicitement les garanties de langage (par exemple, extensions C, unsafePerformIO dans Haskell, conversions de type dangereuses), sinon il serait impossible de tirer des conclusions du tout, et ce message serait assez court. `` En outre, le même Haskell possède un sous-ensemble de Safe Haskell qui interdit explicitement et transitoirement l'utilisation de ces derniers et d'un certain nombre d'autres astuces qui pourraient violer l'intégrité de la langue. ''

Spécification

Qu'une liste et un sens soient donnés. Il est nécessaire de renvoyer l'index de cette valeur dans la liste ou d'indiquer que cette valeur n'est pas dans la liste.

L'implémentation de cette spécification est triviale, il est donc naturel de demander, et voici généralement des tests ou des types. Cependant, ces propriétés et méthodes de raisonnement, dont nous parlerons aujourd'hui, sont applicables à un code beaucoup plus complexe. Laissez l'implémentation prendre dix mille lignes de code spaghetti illisible, si cela aide à voir leur utilité.

Python

 def x(y, z): # 10000    

Nous notons tout de suite que nous ne sommes pas intéressés par les propriétés non contrôlées et n'affectant pas la sémantique d'un programme comme la dénomination des variables et la documentation de texte, donc je n'ai intentionnellement pas écrit de code qui aide à la perception. Nous ne sommes intéressés que par le fait que, sous réserve de réussite aux tests et aux vérifications de type, cela ne peut pas être faux .

Dans le code ci-dessus, il n'y a pratiquement aucune information utile autre que le fait que nous ayons une fonction qui accepte deux arguments. Cette fonction peut également trouver l'index de la valeur dans la liste ou envoyer une lettre insultante à votre grand-mère.

Analyse

Non seulement nous obtenons du code fragile sans tests ni types, mais notre seule façon de comprendre ce que fait une fonction est la documentation. Et comme la documentation est vérifiée par des personnes et non par des machines, elle peut facilement se révéler obsolète «ou initialement incorrecte».

• La documentation
  
  • ✗ Nous connaissons le comportement attendu
    Nous n'avons rien à nous dire sur le comportement de cette fonction. Tu détestes ta grand-mère. Tu es un monstre.
• Garanties
  
  • ✓ Sécurité de la mémoire
    Python est un langage de récupération de place qui nous supprime cette préoccupation. OwCependant, pour autant que je sache, rien ne vous empêche de tirer des bibliothèques dangereuses ou C FFI à l'intérieur de cette fonction. function

Python avec tests

 def test_happy_path(): assert x([1, 2, 3], 2) == 1 def test_missing(): assert x([1, 2, 3], 4) is None 

Maintenant, nous savons que notre fonction fonctionne, et si l'élément est manquant, le résultat est None ?

Et bien non. Ce n'est qu'un exemple. Malheureusement, la portée de notre fonction est infinie, et aucun nombre d'exemples ne peut prouver le bon fonctionnement de notre fonction. Plus de tests - plus de confiance, mais aucun nombre de tests ne résoudra tous les doutes.

La possibilité que cette fonction renvoie None pour 4 , mais pas pour 5 , semble assez fou, et dans ce cas particulier, c'est très probablement un non-sens. Nous pouvons être satisfaits de notre niveau de foi et nous attarder sur un certain nombre d'exemples. Mais là encore, la publication sera courte, alors imaginons que la mise en œuvre n'est pas si évidente.

Étant donné que les tests ne peuvent pas prouver quelque chose dans le cas général, mais ne montrent que le comportement avec des exemples spécifiques, les tests ne peuvent pas montrer l'absence d'erreurs. Par exemple, aucun test ne montre que notre fonction ne lève jamais d'exception ou n'entre jamais dans le cycle éternel, ou ne contient pas de liens invalides. Il ne peut s'agir que d'une analyse statique.

Cependant, même si les exemples ne sont pas très bons dans le rôle de preuve, ils constituent au moins une bonne documentation. À partir de ces deux exemples, nous pouvons dériver la spécification complète ⟦sous quelques hypothèses a priori supplémentaires - ces deux exemples satisfont également, par exemple, le «counterspec» «trouver l'élément dans le tableau et retourner le précédent, le cas échéant», ce qui m'a pris dix secondes pour inventer .

Analyse

Bien que les tests puissent montrer comment utiliser notre fonction, et donnent également un peu d'assurance que cette fonction fonctionne correctement avec au moins quelques exemples, ils ne peuvent rien prouver sur notre code dans le cas général. Malheureusement, cela signifie que les tests ne contribuent que partiellement à éviter les erreurs.

• La documentation
  
  • ✓ Nous avons un exemple d'utilisation
  • ✓ Nous connaissons certaines classes de valeurs qui seront traitées correctement
  • ✗ Nous connaissons tous les types de valeurs qui seront traitées correctement
    Nous n'avons aucune restriction sur les types d'arguments, donc malgré l'existence d'exemples de ce que la fonction peut gérer, nous ne savons pas quels types n'ont pas été testés.
  • ✗ Nous connaissons le comportement attendu
    ⟦L'auteur de l'article original coché ici, je me permettrai de mettre une croix, compte tenu du commentaire ci-dessus⟧
• Spécification
  
  • ✓ Fonctionne dans au moins un cas
  • ✗ L'index retourné est toujours un index valide
  • ✗ L'index renvoyé indique toujours une valeur appropriée
  • Item L'élément manquant renvoie toujours None / Nothing
• Erreurs courantes
  
  • ✗ Pas de fautes de frappe ou de noms incorrects
    L'analyse statique peut aider, mais comme Python est un langage dynamique avec la possibilité de remplacer diverses choses au moment de l'exécution, nous ne pouvons jamais prouver qu'il n'y a pas d'erreur.
    En particulier, il peut être très difficile, voire impossible, de déterminer si le nom de la méthode est correct, car la validité de l'appel de méthode dépend du type d'exécution de l'objet sur lequel l'appel est effectué.
  • ✗ Pas de null inattendu
  • ✗ Le cas d'erreur est toujours traité
    D'après mon expérience, c'est l'une des sources d'erreurs les plus courantes: dans notre exemple, la fonction retourne None en cas d'élément manquant, mais le code utilisant cette fonction peut supposer, par exemple, qu'elle retournera toujours un nombre. En outre, cela peut également entraîner une exception non gérée.
• Garanties
  
  • ✓ Sécurité de la mémoire
  • ✗ La fonction ne peut pas être appelée avec le mauvais type
  • ✗ Aucun effet secondaire
  • ✗ Aucune exception
  • ✗ Aucune erreur
  • ✗ Pas de cycles perpétuels

Haskell

 xyz = -- 10000   

Si vous n'êtes pas familier avec la syntaxe: c'est la définition d'une fonction x avec les paramètres y et z . Dans Haskell, vous pouvez omettre les types, car ils seront déduits de l'implémentation «à moins, bien sûr, que vous n'utilisiez des fonctionnalités avancées différentes des extensions modernes du système de types».

Il peut sembler que ce n'est pas très différent de la version Python, mais seulement parce que nous avons écrit notre fonction en Haskell et qu'elle est en mosaïque, nous pouvons déjà parler de certaines propriétés intéressantes.

Analyse

Évidemment, nous ne pouvons pas tirer autant de conclusions ici, mais voici quelques points à noter:

• La documentation
  
  • ✗ Nous connaissons le comportement attendu
• Erreurs courantes
  
  • ✓ Pas de fautes de frappe ou de noms incorrects
    Étant donné que Haskell est un langage compilé, tous les noms doivent être résolus au moment de la compilation. Le programme ne compilera tout simplement pas s'il y a cette erreur.
  • ✓ Pas de null inattendu
    Haskell n'a tout simplement pas null . Le problème est résolu!
• Garanties
  
  • ✓ Sécurité de la mémoire
  • ✓ La fonction ne peut pas être appelée avec le mauvais type
  • ✓ Aucun effet secondaire inattendu
    ⟦L'auteur de l'article d'origine n'a pas précisé cet élément, mais je me permettrai de noter que s'il y a des effets secondaires, le type déduit de cette fonction indiquera leur présence, afin que le code appelant connaisse leurs capacités.⟧

Type Haskell spécifiant

 x :: Eq a => [a] -> a -> Maybe Int xyz = -- ... 

Plus tôt, nous avons parlé d'une attitude plutôt complice à l'égard de la sécurité des grands-mères: il était clair d'après les tests que la fonction n'allait nuire à personne, mais la grand - mère était -elle vraiment en sécurité? Cette fonction n'envoie-t-elle avec précision aucune lettre de serment?

Haskell est connu pour être un pur langage fonctionnel. Cela ne signifie pas que le code ne peut pas avoir d'effets secondaires, mais tous les effets secondaires doivent être présents dans le type. Nous connaissons le type de cette fonction, nous voyons qu'elle est propre, donc nous sommes sûrs que cette fonction ne modifie aucun état externe.

C'est une propriété très intéressante pour d'autres raisons: comme nous savons qu'il n'y a pas d'effets secondaires, nous pouvons comprendre ce que fait cette fonction, en se basant uniquement sur sa signature! Recherchez simplement cette signature Hoogle et regardez le premier résultat. Bien sûr, ce n'est pas la seule fonction possible qui aurait un tel type, mais le type nous donne suffisamment de confiance pour les besoins de la documentation.

Analyse

• La documentation
  
  • ✓ Nous connaissons le comportement attendu
  • ✗ Nous avons un exemple d'utilisation
  • ✓ Nous connaissons certaines classes de valeurs qui seront traitées correctement
  • ✓ Nous connaissons tous les types de valeurs qui seront traitées correctement
• Spécification
  
  • ✗ Fonctionne dans au moins un cas.
    En l'absence de tests ou de preuves, nous ne savons pas si notre fonction fonctionne du tout comme nous l'attendons!
  • ✗ L'index renvoyé est toujours un index valide.
  • ✗ L'index renvoyé indique toujours une valeur appropriée.
  • ✗ Un élément manquant renvoie toujours None / Nothing .
• Erreurs courantes
  
  • ✓ Pas de fautes de frappe ou de noms incorrects
  • ✓ Pas de null inattendu
  • ✓ Le cas d'erreur est toujours traité
    Si notre fonction retourne Nothing , le système de type s'assure que ce cas est correctement géré par le code appelant. Bien sûr, ce cas peut être ignoré, mais cela doit être fait explicitement.
• Garanties
  
  • ✓ Sécurité de la mémoire
  • ✓ La fonction ne peut pas être appelée avec le mauvais type
  • ✓ Pas d'effets secondaires
  • ✗ Aucune exception
    Je partage des exceptions et des erreurs, croyant qu'après des exceptions, il est possible de récupérer, et après des erreurs (par exemple, des fonctions partiellement définies) - non.
    Pour la plupart, les exceptions sont décrites dans les types (par exemple, dans la monade IO). Dans le bon sens, nous devons savoir qu'une fonction ne lèvera pas d'exception, uniquement sur la base de son type. Cependant, Haskell rompt cette attente en permettant de lever des exceptions à partir de code pur .
    `` De plus, il convient de noter que dans Haskell, des erreurs comme l'appel incorrect de fonctions partiellement définies sont également présentées comme des exceptions qui peuvent être interceptées et traitées, de sorte que la différence entre les deux catégories est légèrement moins évidente.
  • ✗ Aucune erreur
    Nous pouvons toujours utiliser des fonctions partiellement définies, par exemple, la division par zéro.
  • ✗ Pas de cycles perpétuels

Haskell avec tests

Rappelez-vous, j'ai dit plus tôt que les tests ne peuvent pas prouver l'absence d'erreurs? J'ai menti. Lorsque les étoiles convergent correctement, et si les tests sont combinés avec des types, alors cela devient possible! La première étoile est la finitude du domaine de notre fonction. Deuxièmement, le domaine de la définition doit être non seulement limité, mais également pas très étendu, sinon un tel test sera difficile à mettre en pratique.

Par exemple:

 not :: Bool -> Bool not x = ... 

L'entrée peut être True ou False . Il suffit de tester ces deux options, et le voici, le Saint Graal! Aucune exception, cycles perpétuels, résultats incorrects, aucune erreur. OwCependant, pour une fonction un peu plus complexe, il peut ne pas être clair combien de temps est consacré aux tests: s'ils prennent beaucoup de temps, alors nous sommes-nous retrouvés dans un cycle éternel, ou est-ce juste lourd? Le problème de l'arrêter.⟧

En fait, cela n'est pas non plus entièrement vrai dans le cas de Haskell: dans chaque type de Haskell, il y a aussi une valeur ⊥ (qui peut être obtenue comme undefined , error ou, dans un certain sens, comme récursion infinie), mais les Haskellistes ferment traditionnellement les yeux et croient que cela n'existe pas.

Lecture parascolaire: il n'y a que quatre milliards de flotteurs - alors testez-les tous!

Dans tous les cas, dans notre exemple d'origine, la portée est infinie, donc les tests ne peuvent montrer que notre code fonctionne pour un ensemble fini d'exemples.

Analyse
Dans ce cas, les tests complètent les types et bouchent certains trous dans le système de type Haskell. Nous avons beaucoup plus confiance en notre code que d'utiliser uniquement des tests ou des types.

C

 /* C    ,    int */ int x(int *y, size_t n, int z) { /* 10000    */ } 

Nous considérons C par intérêt pour les systèmes de type ancien. En C, en particulier, les types sont très probablement nécessaires non pas au programmeur, mais au compilateur pour l'aider à générer du code plus rapidement.

Dans notre exemple, nous ne savons pas ce que la fonction retournera si l'élément n'est pas trouvé. Nous devrons nous fier à la tradition ou à la documentation (par exemple, dans ce cas, il peut être -1 ).

Nous pourrions également utiliser des arguments out: de cette façon, nous pouvons retourner une erreur et stocker la valeur de retour dans cet argument out. C'est une option un peu plus expressive, mais nous devons encore nous fier à la documentation pour comprendre quels paramètres sont lus et lesquels sont écrits. Dans les deux cas, il est difficile de comprendre le comportement en examinant les types.

 /*   ,   out- */ error_t x(int *y, size_t n, int z, size_t *w) { /* 10000    */ } 

Analyse
Le système de typage lui-même ne nous donne pas autant de garanties. Bien sûr, nous obtenons des informations de ces types, mais il suffit de les comparer avec l'affaire Haskell.

Idris

 x : Eq x => List x -> x -> Maybe Int xyz = ... 

Cette fonction est du même type que dans le cas de Haskell. Cependant, avec un système de type plus expressif, nous pouvons faire plus. Le choix des types peut parler de l'implémentation.

 %default total x : Eq x => Vect nx -> x -> Maybe (Fin n) xyz = ... 

Ce type peut être lu comme «donnez-moi une liste de taille n et une certaine valeur, et je vous retournerai soit un nombre inférieur à n ou Nothing ». Cela garantit que la fonction renvoie un index qui ne dépasse évidemment pas les limites.

De plus, cette fonction est totale, c'est-à-dire que la minuterie a vérifié qu'elle se termine toujours. Cela élimine les cycles perpétuels et les erreurs.

Analyse

• Spécification
  
  • ✗ Fonctionne dans au moins un cas.
  • ✓ L' index retourné est toujours l'index correct
  • ✗ L'index renvoyé indique toujours une valeur appropriée
  • Item L'élément manquant renvoie toujours None / Nothing
• Garanties
  
  • ✓ Sécurité de la mémoire
  • ✓ La fonction ne peut pas être appelée avec le mauvais type
  • ✓ Pas d'effets secondaires
  • ✗ Aucune exception
  • ✓ Aucune erreur
  • ✓ Pas de cycles perpétuels

Idris avec tests

Puisque le langage de type d'Idris est aussi expressif que le langage de ses termes ⟦(ou plutôt, sa partie prouvée totale)⟧, la distinction entre test et type est floue:

 ex : x [1, 2, 3] 2 = Just 1 ex = Refl 

Cette fonction a un type plutôt étrange x [1, 2, 3] 2 = Just 1 . Ce type signifie que pour une vérification de type réussie, le typer doit prouver que x [1, 2, 3] 2 structurellement égal à Just 1 . ⟦Dans ce cas, la preuve est triviale, car il suffit que le basculeur normalise les termes des deux côtés du signe égal, ce qui se fera en temps fini en raison de la totalité de toutes les fonctions utilisées, et qui conduira à un résultat unique grâce à Church-Rosser. Après cela, on peut utiliser la réflexivité de l'égalité, qui est ce que Refl .⟧

En fait, nous avons écrit un test de niveau type.

Idris avec des preuves

Pour l'exhaustivité de l'analyse, nous pouvons utiliser toute la puissance des types dépendants et prouver notre implémentation (puisque les types dépendants dans Idris sont équivalents à un système logique qui inclut une logique constructive de premier ordre).

En particulier, nous pouvons prouver des propriétés qui nous étaient auparavant inaccessibles:

 --      Eq  DecEq x : DecEq a => Vect na -> (y : a) -> Maybe (Fin n) xyz = ... --    ,       `x` findIndexOk : DecEq a => (y : Vect na) -> (z : a) -> case xyz of Just i => index iy = z Nothing => Not (Elem zy) findIndexOk yz = ... 

Le type findIndexOk peut être lu comme «pour tout type a tel qu'il ait une comparaison algorithmiquement décidable ( DecEq ) pour lui, pour tout vecteur y éléments de type a n'importe quelle longueur n et de toute valeur z type a : si xyz renvoie l'index i , alors cet index se trouve z , mais si xyz Nothing renvoie Nothing , alors il n'y a pas un tel élément dans le vecteur. "

`` Il est intéressant de noter que l'auteur de l'article original donne un type légèrement plus faible que celui donné ci-dessus. ''

Maintenant, nous avons tout capturé! Quels sont les inconvénients? Eh bien, écrire toutes ces preuves peut être assez difficile.

Comparaison

Opinion

À mon avis, l'utilisation d'un système de type moderne est en soi la plus efficace en termes de relation entre les informations reçues et les garanties des efforts déployés. Si vous voulez écrire du code assez fiable, les types peuvent être assaisonnés avec des tests. Idéalement - dans le style de QuickCheck.

Avec les types dépendants, la ligne entre les tests et les types devient moins évidente. Si vous écrivez un logiciel pour Boeing ou pour stimulateurs cardiaques, il peut être utile de rédiger des preuves.