You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
65 lines
5.1 KiB
65 lines
5.1 KiB
\section{À propos des méthodes formelles}
|
|
|
|
\subsection{Trouver l'erreur}
|
|
|
|
Lorsqu'on exécute un programme informatique que l'on vient d'écrire, il est courant que le résultat ne soit pas celui que l'on souhaitait. Le plus souvent, cela est dû à une erreur dans le code source du programme, parfois dans les bibliothèques que l'on utilise, rarement dans le compilateur et presque jamais dans le matériel.
|
|
|
|
Cela peut s'expliquer en partie par le fait que le compilateur est utilisé par un plus grand nombre d'utilisateurs que les bibliothèques, lesquelles sont elles-mêmes plus utilisées que notre programme.
|
|
|
|
Faut-il alors attendre qu'un utilisateur de notre programme remarque un bug pour pouvoir le corriger ? Dans le cas des systèmes critiques — transports, énergie, santé etc. — il est impératif de pouvoir détecter les problèmes avant qu'ils ne se manifestent ; dans le cas des autres logiciels, on préfère aussi que cela soit le cas même si ce n'est pas une condition nécessaire.
|
|
|
|
\subsection{Tests manuels et unitaires}
|
|
|
|
Un des moyens de détecter les bugs, est tout simplement de \emph{tester} les programmes. Cela peut se faire à la main, mais cette façon de faire devient très vite fastidieuse dans le cas de gros programmes. On peut donc automatiser les tests. Les tests unitaires sont un exemple de tests automatisés, il s'agit par exemple d'écrire un ensemble de tests pour chacune des fonctions de notre programme. Une fois les tests écrits, on peut ainsi vérifier rapidement que le programme passe les tests, ce qui s'avère pratique lorsque l'on modifie le code du programme par exemple.
|
|
|
|
Cependant, avec cette méthode, si l'on oublie un cas particulier dans nos tests, on aura l'impression que le programme est correct, alors qu'il ne l'est pas. Prenons par exemple cet algorithme écrit en \href{https://ocaml.org/index.fr.html}{\bsc{oc}aml} qui recherche l'entier maximum d'une liste supposée non-vide:
|
|
|
|
\inputminted[bgcolor=darkBackground]
|
|
{ocaml}
|
|
{max_in_list.ml}
|
|
|
|
Supposons que l'on ait écrit les tests suivants pour notre algorithme:
|
|
|
|
\inputminted[bgcolor=darkBackground]
|
|
{ocaml}
|
|
{test_max_in_list.ml}
|
|
|
|
Notre algorithme ne va échouer sur aucun des tests et l'on pourrait alors croire qu'il est correct. Ce n'est bien évidemment pas le cas. Si notre liste n'est composée que de nombres entiers négatifs, l'algorithme renverra $0$ dans tous les cas\textellipsis\ Le test suivant aurait pu détecter cela:
|
|
|
|
\inputminted[bgcolor=darkBackground]
|
|
{ocaml}
|
|
{test_max_in_list_bis.ml}
|
|
|
|
Une version correcte de l'algorithme serait:
|
|
|
|
\inputminted[bgcolor=darkBackground]
|
|
{ocaml}
|
|
{max_in_list_correct.ml}
|
|
|
|
On voit bien alors une des faiblesses des tests: on ne peut jamais être certain d'avoir pensé à tous les cas et on ne peut généralement pas tous les tester lorsqu'il y en a une infinité ou qu'ils sont trop nombreux.
|
|
|
|
\subsection{Un exemple de méthode formelle}
|
|
|
|
Il existe un autre ensemble de façons de procéder, que l'on appelle méthodes formelles. Ces méthodes permettent de vérifier que pour n'importe quel cas, on aura bien le comportement attendu. On peut par exemple exprimer le résultat attendu sous forme de formules logiques, puis, laisser un outil analyser notre programme et nous dire s'il satisfait bien ces formules. Le fait de décrire le comportement attendu sous forme de formules logiques est appelé la \emph{spécification}.
|
|
|
|
Prenons l'exemple de recherche du maximum dans une liste d'entiers supposée non-vide. Avec $l$ la liste passée à notre fonction et $r$ son résultat, la spécification pourrait être la suivante:
|
|
|
|
\[ \forall x \in l, r \geq x \]
|
|
|
|
Si l'outil chargé de vérifier que notre programme satisfait bien cette formule nous affirme que la spécification est respectée, on a alors de fortes garanties sur la \emph{correction} de celui-ci, puisqu'en effet, on reste très général sur notre liste: on ne se réduit pas à quelques cas comme précédemment avec les tests.
|
|
|
|
Cependant, si on y regarde de plus près, on s'aperçoit que le programme suivant satisfait aussi cette formule:
|
|
|
|
\inputminted[bgcolor=darkBackground]
|
|
{ocaml}
|
|
{max_in_list_plus_one.ml}
|
|
|
|
Ici, le problème n'est donc plus celui des cas particuliers, mais celui de la spécification : ici, on a oublié de préciser que la valeur renvoyée par notre fonction doit être présente dans la liste. Cela pourrait s'exprimer ainsi:
|
|
|
|
\[ r \in l \]
|
|
|
|
Il est intéressant de noter que le fait que l'algorithme précédent est incorrect aurait été détecté très facilement avec un test.
|
|
|
|
\subsection{Les différents aspects des méthodes formelles}
|
|
|
|
Les méthodes formelles ne se limitent pas à la vérification d'une spécification pour un algorithme. On peut aussi prouver des propriétés diverses sur des langages, garantir que les états d'un système respectent des contraintes, démontrer des théorèmes mathématiques. Tout cela implique de nombreux travaux tels que le développement de langages de spécification adaptés à des langages particuliers, de solveurs, la formalisation de la sémantique de langages etc. % TODO: reformuler ça %
|
|
|