La preuve de programme vous fera apprécier les tests

William Bartlett Preuve ou test ? 1 / 13

La preuve de programme vous fera apprécier les tests William Bartlett @ w.bartlett@zenika.fr Mastodon Github LINKEDIN punkstarman  William Bartlett Preuve ou test ? 2 / 13

Commençons par pourquoi ? I Les tests automatisés ne sont pas si répandus que ça 1 2018. Borle et al. Analyzing the effects of test driven development in GitHub. William Bartlett Preuve ou test ? 3 / 13

Commençons par pourquoi ? I Les tests automatisés ne sont pas si répandus que ça I Le TDD encore moins 1 1 2018. Borle et al. Analyzing the effects of test driven development in GitHub. William Bartlett Preuve ou test ? 3 / 13

Commençons par pourquoi ? I Les tests automatisés ne sont pas si répandus que ça I Le TDD encore moins 1 I Vous péter le cerveau avec un sujet ésotérique 1 2018. Borle et al. Analyzing the effects of test driven development in GitHub. William Bartlett Preuve ou test ? 3 / 13

Le test logiciel, un vaste sujet I Un monde à part entière William Bartlett Preuve ou test ? 4 / 13

Le test logiciel, un vaste sujet I Un monde à part entière I Des techniques propres William Bartlett Preuve ou test ? 4 / 13

Le test logiciel, un vaste sujet I Un monde à part entière I Des techniques propres I Des choix à faire William Bartlett Preuve ou test ? 4 / 13

Le test logiciel, un vaste sujet I Un monde à part entière I Des techniques propres I Des choix à faire William Bartlett Preuve ou test ? 4 / 13

Le test logiciel, un vaste sujet I Un monde à part entière I Des techniques propres I Des choix à faire MEDIUM Ce ne sont pas les tests que vous recherchez William Bartlett Preuve ou test ? 4 / 13

Et si c’était pire ? Critères Communs et Evaluation Assurance Level (EAL) I EAL1 : testé fonctionnellement I EAL2 : testé structurellement I EAL3 : testé et vérifié méthodiquement I EAL4 : conçu, testé et vérifié méthodiquement I EAL5 : conçu de façon semi-formelle et testé I EAL6 : conception vérifiée de façon semi-formelle et système testé I EAL7 : conception vérifiée de façon formelle et système testé William Bartlett Preuve ou test ? 5 / 13

Exemples I EAL4 / EAL4+ : OS I EAL5 : Smartcard I EAL6 ou EAL7 : Météor (L14) William Bartlett Preuve ou test ? 6 / 13

Comparons Algorithme de tri fusion. I cas de tests automatisés I test de propriétés automatisés I preuve formelle William Bartlett Preuve ou test ? 7 / 13

Tests automatisés Démo William Bartlett Preuve ou test ? 8 / 13

Preuve formelle a: A ⇒ f: a -> b ∧ (x, y): a * b ∨ Left x: a + b

(): () ⊥ _: Empty / Right x: a + b _: a Correspondance Curry-Howard William Bartlett Preuve ou test ? 9 / 13

Exemple Implémentez une fonction : William Bartlett × → × Preuve ou test ? 10 / 13

Exemple Implémentez une fonction : × → × Python : def f(p): return (p[1], p[0]) OCaml : let f (a, b) = (b, a) William Bartlett Preuve ou test ? 10 / 13

Exemple Implémentez une fonction : × → × Python : def f(p): return (p[1], p[0]) OCaml : let f (a, b) = (b, a) Prouvez que, pour toutes propositions , , William Bartlett Preuve ou test ? ∧ ⇒ ∧ 10 / 13

Fonctions totales ∀ , ( ( )) ( ) bien défini ? def f(x): return f(x) La fonction f I ne termine pas I a tous les types I est une preuve de ⊥ MINUS-CIRCLE Toute fonction récursive doit terminer. William Bartlett Preuve ou test ? 11 / 13

Démo William Bartlett Preuve ou test ? 12 / 13

Conclusion I Le test c’est bien I Le test c’est une compétence à part entière I Le test c’est plus facile que la preuve William Bartlett Preuve ou test ? 13 / 13

Conclusion I Le test c’est bien I Le test c’est une compétence à part entière I Le test c’est plus facile que la preuve Pour aller jusqu’à 11 I File Cours de CIS UPenn en libre accès I User Hillel Wayne I Youtube Cours de Xavier Leroy au Collège de France William Bartlett Preuve ou test ? 13 / 13