🧑‍🎤🎸 La preuve de programme vous fera apprécier les tests

William Bartlett Preuve ou test ? 1 / 12

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

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 / 12

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 / 12

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 / 12

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

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

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 / 12

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 / 12

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 / 12

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

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 / 12

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

Preuve formelle A⇒B f: a -> b A∧B (x, y): a * b A∨B Left x: a + b William Bartlett Right x: a + b Preuve ou test ? 9 / 12

Déduction naturelle introduction élimination Γ, A A ∧ ∨ ⇒ ⊥ ΓA ΓB ΓA∧B ΓA ΓB ΓA∨B ΓA∨B Γ, A B ΓA⇒B ΓA Γ ¬A Γ⊥ William Bartlett ΓA∧B ΓA∧B ΓA ΓB ΓA∨B Γ, A C Γ, B C ΓC ΓA ΓA⇒B ΓB Γ⊥ ΓA Preuve ou test ? 10 / 12

Fonction totale et ordre bien-fondé ∀x, P(f (x)) f (x) bien défini ? Toute fonction récursive doit terminer. William Bartlett Preuve ou test ? 11 / 12

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 ? 12 / 12

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 −→ Software Foundations. CIS UPenn. William Bartlett Preuve ou test ? 12 / 12