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

A presentation at Touraine Tech in February 2024 in Tours, France by William Bartlett

Slide 1

Slide 1

William Bartlett Preuve ou test ? 1 / 12

Slide 2

Slide 2

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

Slide 3

Slide 3

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

Slide 4

Slide 4

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

Slide 5

Slide 5

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

Slide 6

Slide 6

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

Slide 7

Slide 7

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

Slide 8

Slide 8

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

Slide 9

Slide 9

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

Slide 10

Slide 10

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

Slide 11

Slide 11

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

Slide 12

Slide 12

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

Slide 13

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

Slide 14

Slide 14

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

Slide 15

Slide 15

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

Slide 16

Slide 16

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

Slide 17

Slide 17

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

Slide 18

Slide 18

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

Slide 19

Slide 19

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