Tester ne peut pas tout essayer
Dans un jeu, deux joueurs peuvent prendre le dernier billet au même instant. Tu testes mille fois et ça marche. Le bug demande un ordre précis d’événements, et il apparaît à la mille et unième. Une méthode formelle n’essaie pas des cas. Elle demande à une machine de les regarder tous.
À la fin de cette leçon
Remarque
Je peux dire ce que rendent un solveur et un vérificateur de modèles quand une propriété est fausse.
Mots-clés
- Propriété : une affirmation sur un système qui doit toujours être vraie.
- Solveur : un programme qui trouve des valeurs qui respectent des règles.
- Vérificateur de modèles : un programme qui essaie tous les états qu’un modèle peut atteindre.
- Invariant : une propriété qui doit tenir dans tous les états.
- Contre-exemple : un déroulement qui montre que la propriété est fausse.
- Modèle : une petite description d’un système qui laisse de côté le détail.
Pour commencer : ce que tu sais déjà
Remarque
Réponds dans ta tête. 1. Qu’est-ce qu’une variable ? 2. Qu’est-ce qu’une condition dans un if ? 3. Que peut-il arriver quand deux programmes modifient la même chose en même temps ? Tu as besoin de la troisième réponse dans un instant.
Avant de commencer
Remarque
Appuie sur Démarrer le lab dans la barre en haut de cette leçon. Ce lab est une machine Ubuntu entière, rien que pour toi : elle met un peu plus de temps à démarrer qu’un conteneur. Chaque bouton Exécuter tape sa commande dans le terminal de la machine, l’une après l’autre, dans la même session. Si l’un d’eux dit que la machine démarre encore, attends quelques secondes et appuie de nouveau. Le premier lancement d’un outil Java prend quelques secondes. Pour les regarder, ou pour taper les tiens, appuie sur Ouvrir le terminal dans la barre.
Un solveur trouve des valeurs, ou prouve qu’il n’y en a pas
Z3 est un solveur. Tu lui donnes des règles et il répond sat (satisfaisable : des valeurs conviennent) avec un exemple, ou unsat (aucune valeur ne convient). La première commande affiche la version. La deuxième demande un nombre x supérieur à 3 et inférieur à 6 : Z3 répond sat et donne 4 pour x. La troisième en demande un supérieur à 5 et inférieur à 3 : Z3 répond unsat. C’est ainsi qu’il prouve : pour prouver une affirmation, demande un cas où elle échoue et obtiens unsat.
z3 --versionAffichée ici, non exécutée. Créez un compte gratuit pour appuyer sur Exécuter et la saisir dans le terminal de votre propre labo.
echo '(declare-const x Int) (assert (and (> x 3) (< x 6))) (check-sat) (get-model)' | z3 -inAffichée ici, non exécutée. Créez un compte gratuit pour appuyer sur Exécuter et la saisir dans le terminal de votre propre labo.
echo '(declare-const x Int) (assert (and (> x 5) (< x 3))) (check-sat)' | z3 -inAffichée ici, non exécutée. Créez un compte gratuit pour appuyer sur Exécuter et la saisir dans le terminal de votre propre labo.
Vérifie
Astuce
Z3 répond unsat pour des règles d’un planning. A-t-il trouvé un planning ? Réponse : non. unsat veut dire qu’aucun planning ne respecte toutes les règles : les règles se contredisent.
Un vérificateur de modèles trouve le mauvais ordre
SPIN vérifie des modèles écrits en Promela. Ton lab en a un : deux travailleurs ajoutent 1 à un compteur partagé, avec un verrou qui ne fait encore rien. spinrun construit le vérificateur et l’exécute sur tous les ordres que les travailleurs peuvent prendre. Il affiche assertion violated (inside==1) et errors: 1, et garde une trace. La deuxième commande rejoue cette trace pas à pas : les deux travailleurs ont fait inside = (inside+1) avant que l’un des deux soit sorti.
spinrun formal/spin/main.pmlAffichée ici, non exécutée. Créez un compte gratuit pour appuyer sur Exécuter et la saisir dans le terminal de votre propre labo.
spin -t -p formal/spin/main.pmlAffichée ici, non exécutée. Créez un compte gratuit pour appuyer sur Exécuter et la saisir dans le terminal de votre propre labo.
Une erreur fréquente
Attention
Beaucoup pensent qu’un vérificateur de modèles prouve qu’un programme est correct. Il prouve que le modèle a la propriété que tu as écrite, rien de plus. Un invariant TRUE n’est jamais violé : le vérificateur le passe aussitôt et ne t’apprend rien. La propriété doit dire quelque chose qu’un système défaillant ne respecterait pas.
Un invariant peut être faux d’un bon système
TLA+ décrit un système par des états et des pas, et TLC le vérifie. Le Lock.tla du lab a deux processus qui peuvent chacun être idle, wait ou cs (dans la section critique). Cet invariant dit qu’ils ne sont jamais tous deux en attente. C’est faux même d’un verrou correct : TLC affiche Invariant NotBothWaiting is violated et un contre-exemple de trois états, qui finit avec les deux processus à wait. La vraie tâche du lab est un autre invariant.
tlc formal/tla/Lock NotBothWaitingAffichée ici, non exécutée. Créez un compte gratuit pour appuyer sur Exécuter et la saisir dans le terminal de votre propre labo.
Un contre-exemple peut être un dessin de personnes
Alloy décrit des choses et les liens entre elles, puis cherche un petit exemple qui casse une affirmation. Ici, les choses sont des personnes et qui est l’ami de qui. alloy exécute les deux commandes du fichier. check Symmetric affiche SAT : Alloy a trouvé un contre-exemple, deux personnes dont l’une compte l’autre parmi ses amis et pas l’inverse, montré sous la forme Person$1->Person$0. run Meet affiche SAT aussi : il a trouvé un exemple à regarder. Pour un check, SAT veut dire que l’affirmation est fausse.
alloy formal/alloy/model.alsAffichée ici, non exécutée. Créez un compte gratuit pour appuyer sur Exécuter et la saisir dans le terminal de votre propre labo.
Maintenant, fais le lab
Astuce
Tu as vu un solveur, une trace, un contre-exemple et une instance. Ton lab te demande d’écrire les règles, le verrou, l’invariant et la réparation, puis chaque outil les vérifie. Ouvre le README.md de ton dossier personnel avec cat README.md dans le terminal.
Vérification finale
Astuce
Réponds sans regarder en arrière. 1. Que répond Z3 quand aucune valeur ne respecte les règles ? 2. Qu’est-ce qu’un contre-exemple ? 3. Qu’y a-t-il de faux dans un invariant TRUE ? 4. Pour un check d’Alloy, que veut dire SAT ? Réponses : unsat ; un déroulement qui montre que la propriété est fausse ; il n’est jamais violé, donc il ne prouve rien ; un contre-exemple a été trouvé.
Pour les enseignants
Astuce
Cette leçon est travaillée dans un lab VM : chaque élève a sa propre machine Ubuntu avec quatre outils de vérification, et un bouton Exécuter tape dans son terminal et montre ce qui s’est affiché. Points clés : 1. Un solveur répond sat avec un exemple ou unsat sans exemple. 2. Un vérificateur de modèles essaie tous les ordres d’événements et donne un contre-exemple quand une propriété échoue. 3. Un invariant TRUE ne prouve rien. 4. Un contre-exemple est la preuve de l’outil, et il peut montrer que la propriété était la mauvaise. Erreur fréquente : croire qu’une réussite veut dire que le système est correct. Matériel : le lab et un navigateur ; TLC et Alloy demandent une VM avec un compte connecté, qui peut joindre GitHub. Conseil : avant spinrun, demandez à la classe de trouver à la main le mauvais ordre. Le lab lui-même a une vérification qui exécute chaque outil.