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
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
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
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
Le test logiciel, un vaste sujet I Un monde à part entière
William Bartlett
Preuve ou test ?
4 / 12
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
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
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
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
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
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
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
Tests automatisés
Démo
William Bartlett
Preuve ou test ?
8 / 12
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
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
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
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
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