why3, un outil pour découvrir expérimentalement les variants et invariants

samedi 22 octobre 2022
par  Alain BUSSER

Voici des extraits du programme de NSI en 1re (thèmes programmation, et algorithmes) :

Contenus Capacités attendues Commentaires
Spécification Décrire les préconditions sur les arguments

Décrire des postconditions sur les résultats.
Des assertions peuvent être utilisées pour garantir des préconditions ou des postconditions.
Mise au point de programmes Utiliser des jeux de tests. Le succès d’un jeu de tests ne garantit pas la correction d’un programme.
Tris par insertion, par sélection Décrire un invariant de boucle qui prouve la correction des tris par insertion, par sélection. La terminaison de ces algorithmes est à justifier.
Recherche dichotomique dans un tableau trié Montrer la terminaison de la recherche dichotomique à l’aide d’un variant de boucle. Des assertions peuvent être utilisées.

La preuve de la correction peut être présentée par le professeur.

Mais surtout, au début du thème « algorithmique », on lit

Il est nécessaire de montrer l’intérêt de prouver la correction d’un algorithme [...] en mobilisant la notion d’invariant sur des exemples simples. La nécessité de prouver la terminaison d’un programme est mise en évidence dès qu’on utilise une boucle non bornée [...] grâce à la mobilisation de la notion de variant sur des exemples simples.

Même si l’instruction assert de Python permet de modéliser les préconditions, postconditions et invariants, il s’avère vite nécessaire de distinguer ces notions [1] en cours. Pour cela, l’outil why3 est intéressant parce qu’il permet de tester des variants et invariants (l’humain se contente de proposer un variant, et why3 tente de prouver que c’en est un). De plus, why3 dispose

  • d’un serveur en ligne, qui évite d’avoir à installer quoi que ce soit sur l’ordinateur,
  • d’une version Python, qui évite d’avoir à apprendre un nouveau langage.

Aussi cet outil a-t-il servi de base à l’enseignement de l’algorithmique en 1re NSI.

Licence Creative Commons
Cet article est mis à disposition selon les termes de la Licence Creative Commons Attribution - Partage dans les Mêmes Conditions 2.0 France.

DNB

Cet exercice a été donné au DNB de 2022 (en Polynésie) :

On considère le programme de calcul suivant :

Choisir un nombre Ajouter 5 Soustraire 5 Multiplier les deux résultats Ajouter 25

1. a. Si on choisit le nombre 7, vérifier qu’on obtient 49 à la fin du programme
b. Si on choisit le nombre −4, quel résultat obtient-on à la fin du programme ?
2. On note x le nombre choisi au départ
a. Exprimer en fonction de x le résultat obtenu.
b. Développer et réduire (x + 5)(x − 5).
c. Sarah dit : « Avec ce programme de calcul, quel que soit le nombre choisi au départ, le résultat obtenu est toujours le carré du nombre de départ ».
Qu’en pensez-vous ?

flow974

On peut répondre aux premières questions en reproduisant le diagramme du sujet sur flow974.

Voici la version du sujet :

Choisir un nombre Ajouter 5 Soustraire 5 Multiplier les deux résultats Ajouter 25

Et celle obtenue sur flow974 :

En mettant le premier nombre (en haut à gauche) sur 7, on vérifie (en haut à droite) que le résultat est bien 49. Et en mettant le nombre choisi sur -4

on trouve que le résultat est 16 (qui est bien, comme le prétend Sarah, le carré de -4).

La programmation par flot permet de faire abstraction du fait qu’il y a deux modifications à apporter (augmenter de 5, diminuer de 5). En Python, il faut garder une copie de la valeur initiale du nombre choisi (ou, ce qui revient au même, une autre variable) pour mémoriser cette valeur initiale. On montre dans les onglets suivants comment faire.

Sofus

Pour traduire en Python, on peut utiliser SofusPy974 où on crée une copie qu’on modifie en place :

SofusPy974 est doté d’un bouton Python, (appelé éditeur) à cliquer pour obtenir automatiquement ce script :

  1. def sarah(nombre):
  2.    copie = nombre
  3.     nombre = nombre + 5
  4.     copie = copie - 5
  5.     nombre = nombre * copie
  6.     nombre = nombre + 25
  7.     return nombre

Télécharger

pseudocode

SofusPy974 a aussi un bouton donnannt directement ce pseudocode :

algorithme sarah(nombre)
   copie ← nombre
   nombre ← nombre + 5
   copie ← copie - 5
   nombre ← nombre × copie
   nombre ← nombre + 25
   renvoyer nombre

Pour répondre aux questions de l’exercice, on entre dans une console

  1. >>> sarah(7)
  2. 49
  3. >>> sarah(-4)
  4. 16
  5. >>>

Télécharger

Mais cela ne permet pas de prouver l’affirmation de Sarah. Pour une preuve utilisant directement le calcul formel, on peut utiliser Sofus (sans Python), qui permet de manipuler aussi des expressions littérales :

On voit dans l’affichage en bas que l’image de 7 par la fonction est 49. Pour avoir l’image de x par cette fonction, il suffit de remplacer 7 par x :

Ceci prouve l’affirmation de Sarah. Mais sans expliquer pourquoi. On verra plus loin que why3 fait pareil, malgré ce que son nom laisse penser : il donne un certificat sans qu’on aie besoin de vérifier pourquoi. On va donc aider Sarah à obtenir ce certificat, en programmant sa fonction en Python puis en la soumettant à why3.

Python

Sarah programme sa fonction en Python. En voyant le schéma

Choisir un nombre Ajouter 5 Soustraire 5 Multiplier les deux résultats Ajouter 25

elle décide de créer deux nouvelles variables, correspondant aux deux facteurs du produit. Elle appelle facteur1 celle qui est à gauche et facteur2 celle qui est à droite :

  1. def sarah(nombre):
  2.     facteur1 = nombre+5
  3.     facteur2 = nombre-5
  4.     produit = facteur1 * facteur2
  5.     return produit+25

Télécharger

On peut alors vérifier, en mode pas-à-pas, sur Pythontutor :

Mais cela ne prouve pas l’affirmation de Sarah dans tous les cas. C’est là que why3 entre en scène.

why3

L’affirmation de Sarah est simplement un commentaire dans le script Python :

  1. def sarah(nombre):
  2.     #@ ensures result == nombre*nombre
  3.     facteur1 = nombre+5
  4.     facteur2 = nombre-5
  5.     produit = facteur1 * facteur2
  6.     return produit+25

Télécharger

Mais ce commentaire débute par un arobase, ce qui lui donne un sens pour why3. Le mot-clé result désigne ce qui est renvoyé par la fonction. En copiant ce script sur le site de why3 on a

Pour demander une certification de la fonction, il suffit alors de cliquer sur la baguette magique et why3 s’occupe du reste :

Mais malgré son nom, why3 se contente de donner un certificat : Sarah a raison, et n’explique pas pourquoi elle a raison. Pour en savoir un peu plus, on peut cliquer sur l’icône représentant un arbre, ce qui a pour effet de séparer le but à prouver en sous-buts :

On en sait maintenant plus : si l’affirmation de Sarah est vraie, c’est parce qu’elle correspond à une postcondition et c’est une postcondition que why3 a prouvé.

Pour prouver une postcondition sur une fonction Python, on ajoute au début de la définition de cette fonction, un commentaire de ce genre :

#@ ensures la_condition

où la_condition est un booléen de Python, puis on copie le script sur why3 en Python et on clique sur la baguette magique.

Post

Pour initier les élèves de 1re aux variants et invariants dès le début de l’année scolaire, il est intéressant de les mettre en œuvre sur des exemples simples, autrement dit, portant sur des types de base (entiers naturels par exemple).

L’exemple des machines à registre, déjà testé avec succès dans le premier degré, s’avère parfait pour cela.

L’activité a été pratiquée tout d’abord en mode débranché (il s’agissait de tester les programmes et émettre des conjectures sur le résultat de l’opération).

Listes

En fait les registres de la machine à registre sont groupés en un tableau d’entiers. Pour modéliser en Python un tel tableau, on utilise des variables numérotées. Par exemple

L = [5,0,3,2]

ce qui revient (une fois L de longueur suffisante) à

  1. L[0] = 5
  2. L[1] = 0
  3. L[2] = 3
  4. L[3] = 2

Télécharger

qu’au début de l’année de 1re on notera

  1. L0 = 5
  2. L1 = 0
  3. L2 = 3
  4. L3 = 2

Télécharger

Ceci aura l’avantage d’éviter de demander à why3 de vérifier que des indices sont bien entre les bornes.

Plus tard on apprend à dessiner un tableau d’entiers naturels avec cette fonction :

  1. def dessiner(tab):
  2.     for n in tab:
  3.         print(n*'o')

Télécharger

Par exemple avec

dessiner( [5,0,3,2] )

on a dans la console

ooooo

ooo
oo

Addition

Le programme d’addition pour la machine à registres (avec seulement L0 et L1 utilisés, le doigt pointant initialement vers L0) est

La première étape est de traduire ce programme en Python.

Tout d’abord, le point d’interrogation en haut mène à

  • un arrêt (sortie de boucle) à gauche, si la première case est vide (L0==0)
  • une boucle (très visible sur la partie droite du graphe) sinon.

En effet dans la boucle, il y a un aller-retour du doigt vers la case L1. C’est bien la non nullité de L0 qui est testée à chaque retour de la boucle.

Le début du script ressemblera donc à

  1. def addition(a,b):
  2.     L0 = a
  3.     L1 = b
  4.     while L0>0:

Télécharger

Reste à détailler ce qu’on fait dans la boucle :

  • on enlève une graine de la première case : L0 -= 1
  • on déplace le doigt vers la droite : maintenant c’est sur la variable L1 qu’on va opérer
  • on sème une graine devant le doigt : L1 += 1
  • on ramène le doigt vers la gauche : on boucle bien sur L0

Ce qui donne alors ce script :

  1. def addition(a,b):
  2.     L0 = a
  3.     L1 = b
  4.     while L0>0:
  5.         L0 -= 1
  6.         L1 += 1
  7.     return L1

Télécharger

Comment sait-on que c’est L1 qui contient le résultat de l’addition ? On l’a constaté expérimentalement lors de la phase débranchée de l’activité.

Pour faire certifier qu’il s’agit bien d’une addition, on modifie le script ainsi :

  1. def addition(a,b):
  2.     #@ ensures result==a+b
  3.     L0 = a
  4.     L1 = b
  5.     while L0>0:
  6.         L0 -= 1
  7.         L1 += 1
  8.     return L1

Télécharger

puis on va sur le site why3 (paramétré en Python) et on demande la vérification en cliquant sur la baguette magique.

La magie n’opère pas : why3 ne réussit pas à prouver qu’il s’agit bien d’une addition. On voit d’ailleurs que ce n’est pas le seul problème : why3 a également échoué à prouver que l’algorithme se termine !

En ce qui concerne la terminaison, il est impossible de la prouver, parce que l’algorithme ne termine pas !

En effet si on essaye avec des nombres négatifs la condition L0==0 ne sera jamais atteinte.

Ce problème aura plus de chances d’être résolu :

  1. def addition(a,b):
  2.     #@ requires a>=0
  3.     #@ requires b>=0
  4.     #@ ensures result==a+b
  5.     L0 = a
  6.     L1 = b
  7.     while L0>0:
  8.         L0 -= 1
  9.         L1 += 1
  10.     return L1

Télécharger

Mais cela ne suffit toujours pas : pour prouver la terminaison de l’algorithme, why3 a besoin d’un variant. C’est le moment de définir un variant (en 1re) :

Un variant est une expression à valeur entière positive qui décroît strictement à chaque passage dans la boucle

why3 doit vérifier

  • que l’expression proposée est bien un variant
  • qu’elle a une valeur positive au début

et en déduira la terminaison de la boucle, et donc de l’algorithme.

Un variant tout trouvé est la variable L0 qui décroît à chaque passage dans la boucle :

  1. def addition(a,b):
  2.     #@ requires a>=0
  3.     #@ requires b>=0
  4.     #@ ensures result==a+b
  5.     L0 = a
  6.     L1 = b
  7.     while L0>0:
  8.         #@ variant L0
  9.         L0 -= 1
  10.         L1 += 1
  11.     return L1

Télécharger

Maintenant why3 réussit à certifier la terminaison de l’algorithme [2] :

Pour prouver la correction, il faut un invariant. C’est le moment de définir cette notion :

Un invariant est un booléen qui garde la même valeur après chaque passage dans la boucle

Alors si l’invariant s’évalue à True avant d’entrer dans la boucle, il sera True à la sortie de la boucle. Des exemples d’invariants sont proposés :

  1. 2+2==4
  2. a>=0
  3. b>=0
  4. L0>=0
  5. L1>=0
  6. L0+L1==a+b

Télécharger

mais seul le dernier a quelque utilité dans le cas présent :

  1. def addition(a,b):
  2.     #@ requires a>=0
  3.     #@ requires b>=0
  4.     #@ ensures result==a+b
  5.     L0 = a
  6.     L1 = b
  7.     while L0>0:
  8.         #@ variant L0
  9.         #@ invariant L0+L1==a+b
  10.         L0 -= 1
  11.         L1 += 1
  12.     return L1

Télécharger

Mais ça ne suffit toujours pas :

Selon why3, le booléen L0+L1==a+b est bien un invariant, mais il ne sert à rien si on ne peut pas prouver qu’il est vrai au début du script. Or, au début, les variables L0 et L1 sont initialisées à a et b donc L0+L1 est censé valoir a+b. Où est le problème ?

Il semble que why3 utilise un raisonnement par récurrence et on a besoin de prouver que le variant L0 est positif :

  1. def addition(a,b):
  2.     #@ requires a>=0
  3.     #@ requires b>=0
  4.     #@ ensures result==a+b
  5.     L0 = a
  6.     L1 = b
  7.     while L0>0:
  8.         #@ variant L0
  9.         #@ invariant L0>=0
  10.         #@ invariant L0+L1==a+b
  11.         L0 -= 1
  12.         L1 += 1
  13.     return L1

Télécharger

Ce script donne le certificat tant attendu (et mérité, après toutes ces pérégrinations !) :

Soustraction

L’algorithme de soustraction ressemble beaucoup à celui de l’addition :

En fait, la seule différence est qu’au lieu de semer une graine dans la seconde case, on en récolte une. Il suffit donc de remplacer un « + » par un « - » dans le script de l’onglet précédent :

  1. def soustraction(a,b):
  2.     L0 = a
  3.     L1 = b
  4.     while L0>0:
  5.         L0 -= 1
  6.         L1 -= 1
  7.     return L1

Télécharger

Ceci dit, il y a quand même une différence importante par rapport au cas de l’addition : tout élève de cycle 2 sait qu’on ne peut pas soustraire à un entier naturel, un entier plus grand que lui. On a donc besoin d’une précondition supplémentaire ici, à savoir que a est inférieur ou égal à b.

Le script proposé à why3 sera donc :

  1. def soustraction(a,b):
  2.     #@ requires a>=0
  3.     #@ requires b>=0
  4.     #@ requires a<=b
  5.     #@ ensures result==b-a
  6.     L0 = a
  7.     L1 = b
  8.     while L0>0:
  9.         #@ variant L0
  10.         #@ invariant L0>=0
  11.         #@ invariant L0<=L1
  12.         #@ invariant L1-L0==b-a
  13.         L0 -= 1
  14.         L1 -= 1
  15.     return L1

Télécharger

Ce script est certifié :

Multiplication

L’algorithme de multiplication est plus complexe, ne serait-ce que parce qu’il utilise plus de registres (4 au lieu de 2 pour les onglets précédents) :

En suivant les mouvements du doigt entre les points d’interrogation, et partant du fait qu’au début le doigt est tout à gauche, on voit que les boucles portent respectivement sur L0, L1 et L2. La structure générale du programme est

  1. def multiplication(a,b):
  2.     L0 = a
  3.     L1 = b
  4.     L2 = 0
  5.     L3 = 0
  6.     while L0>0:
  7.         ...
  8.         while L1>0:
  9.             ...
  10.         while L2>0:
  11.             ...
  12.     ....
  13.     return L3

Télécharger

On sait que c’est L3 qui contient le produit à la fin, parce qu’on l’a constaté expérimentalement. La suite, c’est de le faire certifier par why3. Comme il y a 3 boucles, on aura a priori besoin de 3 variants.

En lisant les flèches du graphe, on repère quels sont les registres à incrémenter ou décrémenter, ce qui donne cette fonction :

  1. def multiplication(a,b):
  2.     L0 = a
  3.     L1 = b
  4.     L2 = 0
  5.     L3 = 0
  6.     while L0>0:
  7.         L0 -= 1
  8.         while L1>0:
  9.             L1 -= 1
  10.             L2 += 1
  11.             L3 += 1
  12.         while L2>0:
  13.             L2 -= 1
  14.             L1 += 1
  15.     return L3

Télécharger

Les élèves écrivent cela dans un IDE Python, tandis que le graphe est projeté : ils traduisent depuis le graphe, vers le code Python.

Version liste

Lorsque le cours sur les listes a commencé, on peut transformer le programme ci-dessus en

  1. def multiplication(a,b):
  2.     L[0] = a
  3.     L[1] = b
  4.     L[2] = 0
  5.     L[3] = 0
  6.     while L[0]>0:
  7.         L[0] -= 1
  8.         while L[1]>0:
  9.             L[1] -= 1
  10.             L[2] += 1
  11.             L[3] += 1
  12.         while L[2]>0:
  13.             L[2] -= 1
  14.             L[1] += 1
  15.     return L[3]

Télécharger

puis en

  1. def multiplication(a,b):
  2.     L[0] = a
  3.     L[1] = b
  4.     L[2] = 0
  5.     L[3] = 0
  6.     doigt = 0
  7.     while L[doigt]>0:
  8.         L[doigt] -= 1
  9.         doigt += 1
  10.         while L[doigt]>0:
  11.             L[doigt] -= 1
  12.             doigt += 1
  13.             L[doigt] += 1
  14.             doigt += 1
  15.             L[doigt] += 1
  16.             doigt -= 1
  17.             doigt -= 1
  18.         while L[doigt]>0:
  19.             L[doigt] -= 1
  20.             doigt -= 1
  21.             L[doigt] += 1
  22.             doigt += 1
  23.         doigt -= 1
  24.         doigt -= 1
  25.     return L[3]

Télécharger

qui est plus proche du graphe.

Ce script est simplifiable. Par exemple on reconnaît dans la boucle sur L2, l’algorithme d’addition qui a déjà été certifié deux onglets auparavant. Alors on peut remplacer la boucle par la fonction :

  1. def multiplication(a,b):
  2.     L0 = a
  3.     L1 = b
  4.     L2 = 0
  5.     L3 = 0
  6.     while L0>0:
  7.         L0 -= 1
  8.         while L1>0:
  9.             L1 -= 1
  10.             L2 += 1
  11.             L3 += 1
  12.         L1 += L2
  13.         L2 = 0
  14.     return L3

Télécharger

La dernière ligne vient de ce que l’addition détruit le premier opérande (le rend égal à 0). Mais du coup, la variable L2 qui est initialisée à 0, puis remise à 0 après chaque passage dans le boucle sur L1, devient inutile. Ce qui simplifie encore le script :

  1. def multiplication(a,b):
  2.     L0 = a
  3.     L1 = b
  4.     L3 = 0
  5.     while L0>0:
  6.         L0 -= 1
  7.         while L1>0:
  8.             L1 -= 1
  9.             L3 += 1
  10.     return L3

Télécharger

Et maintenant, on reconnaît une nouvelle fois l’algorithme d’addition, dans la boucle sur L1. Ce qui permet une nouvelle simplification du script :

  1. def multiplication(a,b):
  2.     L0 = a
  3.     L1 = b
  4.     L3 = 0
  5.     while L0>0:
  6.         L0 -= 1
  7.         L3 += L1
  8.     return L3

Télécharger

C’est cette dernière version qui a été testée sur why3 :

  1. def multiplication(a,b):
  2.     #@ requires a>=0
  3.     #@ requires b>=0
  4.     #@ ensures result==a*b
  5.     L0 = a
  6.     L1 = b
  7.     L3 = 0
  8.     while L0>0:
  9.         #@ variant L0
  10.         #@ invariant L0>=0
  11.         #@ invariant L0*b+L3==a*b
  12.         L0 -= 1
  13.         L3 += L1
  14.     return L3

Télécharger

Elle est certifiée :

Remarque : On pouvait encore simplifier la fonction, en constatant que la variable L1 n’est pas utile non plus :

  1. def multiplication(a,b):
  2.     #@ requires a>=0
  3.     #@ requires b>=0
  4.     #@ ensures result==a*b
  5.     L0 = a
  6.     L3 = 0
  7.     while L0>0:
  8.         #@ variant L0
  9.         #@ invariant L0>=0
  10.         #@ invariant L0*b+L3==a*b
  11.         L0 -= 1
  12.         L3 += b
  13.     return L3

Télécharger

Cette nouvelle version est également certifiée :

Cette simplification n’a pas été faite en classe (manque de temps) mais un devoir a suivi, portant sur la multiplication éthiopienne :

  1. def multiplication(a,b):
  2.     #@ requires a>=0
  3.     #@ requires b>=0
  4.     #@ ensures result==a*b
  5.     d = a
  6.     p = b
  7.     s = 0
  8.     while d>0:
  9.         #@ variant d
  10.         #@ invariant d>=0
  11.         #@ invariant d*p+s==a*b
  12.         if d%2==1:
  13.             s += p
  14.         d //= 2
  15.         p *= 2
  16.     return s

Télécharger

Ce « nouvel » [3] algorithme de multiplication est également certifié :

Division

L’algorithme de division par soustraction itérée est certifié également par why3 :

  1. def division(a,b):
  2.     #@ requires a>=0
  3.     #@ requires b>0
  4.     #@ ensures result[1]>b
  5.     #@ ensures result[1]>=0
  6.     #@ ensures b*result[0]+result[1]==a
  7.     L = [0,a]
  8.     while L[1]>=b:
  9.         #@ variant L[1]
  10.         #@ invariant L[1]>=0
  11.         #@ invariant b*L[0]+L[1]==a
  12.         L[1] -= b
  13.         L[0] += 1
  14.     return L

Télécharger

On constate qu’il est nécessaire que le diviseur b soit non nul : la division par 0 ne termine pas.

En résumé, why3 est un bureaucrate : on a besoin qu’il donne un coup de tampon pour certifier un algorithme, et lui il réclame d’abord qu’on lui fournisse des formulaires venant de 3 autres bureaux :

  • le bureau des variants (entiers décroissants)
  • le bureau des invariants (booléens croissants)
  • le bureau des postconditions (ensures)
  • et parfois le bureau des restrictions (requires)

Un peu comme ici :

On peut réinvestir les variants et invariants dans la suite du cours, à propos des listes de Python.

Listes

Que dit le programme ?

Contenus Capacités attendues Commentaires
Parcours séquentiel d’un tableau Écrire un algorithme de recherche d’une occurence [...]

Écrire un algorithme de recherche d’un extremum, de calcul d’une moyenne.
On montre que le coût est linéaire

Pas le moindre variant ni invariant ici. Mais comme on en aura besoin plus bas, autant les regarder déjà ici.

in

La recherche d’une occurence peut être comprise de plusieurs manières :

  • dire si elt est dans le tableau
  • dire où (à quel indice ou quels indices) elt est dans tab
  • dire combien de fois elt est dans tab
  • dire quels sont les éléments de tab vérifiant un prédicat donné (par exemple extraire les nombres pairs du tableau).

Toutes ces variantes sont présentes à l’épreuve pratique Python du bac NSI.

Dans le paradigme map-filter-reduce il s’agit d’un filtrage. Plus précisément, pour tester si elt est dans tab,

  • on effectue un filtrage (tester le prédicat « est égal à elt » sur tab avec [x for x in tab if x==elt],
  • puis on réduit avec l’opération or : any([x==elt for x in tab])

Pour tester si elt est dans tab, on pense à une boucle de ce genre :

  1. def est_dedans(elt,tab):
  2.     for x in tab:
  3.         if x==elt:
  4.             return True
  5.     return False

Télécharger

Comme le nombre de passages dans une boucle for est prédéterminé (donc fini), il n’y a pas besoin de prouver la terminaison de l’algorithme. Il n’y a donc que la correction à prouver. Par exemple avec l’affirmation selon laquelle le résultat est True si et seulement s’il existe un indice i tel que l’élément d’indice i dans tab est égal à l’élément cherché :

  1. def est_dedans(elt,tab):
  2.     #@ ensures result <-> exists i. 0<=i<=len(tab) and tab[i]==elt
  3.     for x in tab:
  4.         if x==elt:
  5.             return True
  6.     return False

Télécharger

Mais why3 ne peut pas certifier cet algorithme :

Il lui manque un invariant. Le problème est d’en exprimer un. Celui qui vient naturellement à l’esprit est « on n’a pas encore trouvé elt dans la partie de tab déjà parcourue ». Ne voyant pas comment exprimer cet invariant, on va tout traduire en terme d’indices [4]. La nouvelle version est

  1. def est_dedans(elt,tab):
  2.     #@ ensures result <-> exists i. 0<=i<=len(tab) and tab[i]==elt
  3.     for i in range(len(tab)):
  4.         if tab[i]==elt:
  5.             return True
  6.     return False

Télécharger

Comme prévu why3 ne prouve pas la correction puisqu’il n’a pas d’invariant à se mettre sous la dent :

Mais maintenant on peut exprimer en Python l’invariant :

  1. def est_dedans(elt,tab):
  2.     #@ ensures result <-> exists i. 0<=i<len(tab) and tab[i]==elt
  3.     for i in range(len(tab)):
  4.         #@ invariant forall k. 0<=k<i -> tab[k]!=elt
  5.         if tab[i]==elt:
  6.             return True
  7.     return False

Télécharger

Maintenant why3 certifie l’algorithme :

max

Le maximum d’une liste (d’objets munis d’une relation d’ordre, ici des entiers naturels) s’obtient en utilisant la fonction reduce du trio map-filter-reduce avec l’opération (associative) qui, à deux entiers, associe le plus grand des deux. On convient donc que le maximum d’une liste vide est l’élément neutre de cette opération, à savoir 0 (pour les entiers naturels : on utilise le fait que la relation d’ordre sur les entiers naturels est un bon ordre [5] et que le plus petit entier naturel est 0). La variable m sera donc initialisée à 0.

L’expérience acquise dans l’onglet précédent amène à choisir un parcours de la liste par indice :

  1. def maximum(L):
  2.     #@ requires forall i. 0<=i<len(L) -> L[i]>=0
  3.     #@ ensures forall i. 0<=i<len(L) -> result>=L[i]
  4.     m = 0
  5.     for k in range(len(L)):
  6.         if L[k]>m:
  7.             m = L[k]
  8.     return m

Télécharger

En fait dire que la valeur finale de m est le maximum, c’est dire que

  • d’une part aucun élément de la liste n’est plus grand que m (le ensures ci-dessus)
  • d’autre part que cette valeur est bien dans la liste. On ne le prouve pas ici parce que cela a été vu dans l’onglet précédent.

On s’en doutait, why3 n’arrive pas à prouver la correction :

Le problème est de trouver un invariant. Par exemple celui-là :

  1. def maximum(L):
  2.     #@ requires forall i. 0<=i<len(L) -> L[i]>=0
  3.     #@ ensures forall i. 0<=i<len(L) -> result>=L[i]
  4.     m = 0
  5.     for k in range(len(L)):
  6.         #@ invariant forall i. 0<=i<k -> L[i]<=m
  7.         if L[k]>m:
  8.             m = L[k]
  9.     return m

Télécharger

Avec cet invariant, why3 certifie l’algorithme :

min

La valeur initiale 0 était adaptée pour calculer le maximum d’une liste d’entiers naturels, parce qu’aucun entier naturel n’est plus petit que 0. Pour le minimum d’une liste, on ne peut pas faire pareil : l’élément neutre du minimum est +∞ qui, en Python, est un flottant.

Mais sous réserve que la liste ne soit pas vide, on pouvait également initialiser la variable m au premier élément de la liste [6]. On est donc obligé de préciser que cette nouvelle fonction ne s’applique qu’à des listes non vides (c’est-à-dire de longueur strictement positive) :

  1. def maximum(L):
  2.     #@ requires forall i. 0<=i<len(L) -> L[i]>=0
  3.     #@ requires len(L)>0
  4.     #@ ensures forall i. 0<=i<len(L) -> result>=L[i]
  5.     m = L[0]
  6.     for k in range(len(L)):
  7.         #@ invariant forall i. 0<=i<k -> L[i]<=m
  8.         if L[k]>m:
  9.             m = L[k]
  10.     return m

Télécharger

Cette nouvelle fonction maximum est également certifiée par why3 :

Cette nouvelle fonction maximum peut maintenant être adaptée au minimum d’une liste, simplement en échangeant les < avec des > :

  1. def minimum(L):
  2.     #@ requires forall i. 0<=i<len(L) -> L[i]>=0
  3.     #@ requires len(L)>0
  4.     #@ ensures forall i. 0<=i<len(L) -> result<=L[i]
  5.     m = L[0]
  6.     for k in range(len(L)):
  7.         #@ invariant forall i. 0<=i<k -> L[i]>=m
  8.         if L[k]<m:
  9.             m = L[k]
  10.     return m

Télécharger

Cette fonction minimum est certifiée par why3 :

sum

La fonction qui, à une liste (ici, d’entiers parce qu’on peut additionner des entiers), associe la somme de tous ses éléments, correspond dans le trio map-filter-reduce à un reduce, avec l’opération binaire d’addition. On convient alors que la somme d’une liste vide est égale à 0.

Ce qui donne ce script :

  1. def somme(L):
  2.     s = 0
  3.     for i in range(len(L)):
  4.        s += L[i]
  5.     return s

Télécharger

L’écriture est correcte du point de vue de la syntaxe :

Que prouver ?

  1. def somme(L):
  2.     #@ ensures result==sum(L)
  3.     s = 0
  4.     for i in range(len(L)):
  5.         s += L[i]
  6.     return s

Télécharger

Là ça ne fonctionne pas : why3 ne dispose pas de la fonction sum() de Python :

Comment aolrs prouver qu’une fonction est correcte sans utiliser la fonction ? Il faudrait pour ça récursifier la fonction, ce qui sort du programme de 1re.

Pour l’invariant aussi on a besoin de sum :

  1. def somme(L):
  2.     #@ ensures result==sum(L)
  3.     s = 0
  4.     for i in range(len(L)):
  5.         #@ invariant s==sum([L[j] for j in range(i)])
  6.         s += L[i]
  7.     return s

Télécharger

C’est même l’écriture d’une compréhension qui échappe à why3 :

Tout cela ne donne pas envie d’utiliser why3 pour étudier l’algorithme de sommation. Mais de toute manière

  • cet algorithme est fondamentalement récursif (la somme jusqu’à n, c’est la somme jusqu’à n-1, plus le n-ième terme)
  • et le programme ne cite pas la somme, mais la moyenne : on n’a même pas terminé le travail à ce stade !

Noter qu’en première technologique, en maths, l’algorithme de somme est également au programme, via la notion d’accumulateur.

Bref, il a été fait le choix de ne pas utiliser why3 pour les algorithmes de somme et de moyenne. D’ailleurs le programme précise « sur des exemples simples » et on est en droit de ne pas trouver si simple que cela ces algorithmes...

Maintenant qu’on a fini de traiter les variants et invariant « sur des exemples simples » comme le préconise le programme de 1re, on va passer aux algorithmes sur les listes : tris par insertion et sélection, recherche dichotomique dans une liste triée.

Tris

Au programme de 1re, il y a

  • la preuve de correction du tri par insertion, par un invariant
  • la preuve de correction du tri par sélection, par un invariant
  • la preuve de terminaison de la recherche dichotomique, par un variant

Sélection

Ce script peut être certifié par la version locale de why3 :

  1. def tri_selection(L):
  2.     #@ ensures forall i. forall j. 0<=i<j<len(L) -> L[i]<=L[j]
  3.     im = 0
  4.     for i in range(len(L)):
  5.         #@ invariant forall k. forall l. 0<=k<i<=l<len(L) -> L[k]<=L[l]
  6.         #@ invariant forall k. forall l. 0<=k<=l<i -> L[k]<=L[l]
  7.         im = i
  8.         for j in range(i+1,len(L)):
  9.             #@ invariant i<=im<j
  10.             #@ invariant forall k. i<=k<j -> L[im]<=L[k]
  11.             if L[j]<L[im]:
  12.                 im = j
  13.         if im != i:
  14.             L[im], L[i] = L[i], L[im]
  15.         #@ assert forall k. 0<=k<i -> L[k]<=L[i]

Télécharger

Mais la version en ligne utilisant l’excellent mais insuffisant Alt-Ergo ne réussit pas à valider cet algorithme.

En résumé l’invariant « le début de la liste est déjà trié » ne suffit pas, il faut également prouver que tous ses éléments sont inférieurs à tous les éléments restant à trier. On voit là un réel intérêt de why3, dont la pratique montre la nécessité de ce second invariant.

Insertion

Pour effectuer un tri par insertion en place, on décale vers la droite les éléments du tableau jusqu’à ce qu’on trouve un élément devant lequel placer celui qui était à la fin du tableau :

  1. def tri_par_insertion(t):
  2.     #@ ensures forall i. forall j. 0<=i<j<len(t) -> t[i]<=t[j]
  3.     for i in range(1, len(t)):
  4.         #@ invariant forall k. forall l. 0<=k<l<i -> t[k]<=t[l]
  5.         j = i
  6.         while j>0 and t[j-1]>t[i]:
  7.             #@ variant j
  8.             #@ invariant 0<=j<=i
  9.             #@ invariant forall k. forall l. 0<=k<l<=i and k!=j and l!=j -> t[k]<=t[l]
  10.             #@ invariant forall k. j+1<=k<=i -> t[i]<=t[k]
  11.             t[j] = t[j-1]
  12.             j -= 1
  13.         t[j] = t[i]

Télécharger

(à vérifier avec why3)

On constate que « le début de la liste est trié » est un invariant commun aux deux algorithmes de tri au programme de 1re.

On constate également qu’il est nécessaire ici de prouver aussi la terminaison de l’algorithme. Un variant est assez facile à trouver [7]

On peut tenter aussi cette version avec échanges (plutôt que décalages) :

  1. def tri_insertion(L):
  2.     #@ ensures forall i. forall j. 0<=i<j<len(L) -> L[i]<=L[j]
  3.     for i in range(1,len(L)):
  4.         #@ invariant forall k. forall l. 0<=k<l<i -> L[k]<=L[l]
  5.         #@ invariant forall k. forall l. 0<=k<i<=l<len(L) -> L[k]<=L[l]
  6.         j = i
  7.         while j>0 and L[j-1]>=L[j]:
  8.             #@ invariant 0<=j<=i
  9.             #@ invariant forall x. forall y. 0<=x<y<=i and y!=j -> L[x]<=L[y]
  10.             #@ variant j
  11.             L[j-1],L[j] = L[j],L[j-1]
  12.             j -= 1

Télécharger

Dichotomie

Cet algorithme de recherche dichotomique dans une liste triée (préassertion) a été certifié par why3

  1. def recherche(lst, x):
  2.     #@ requires forall i. forall j. 0 <= i < j < len(lst) -> lst[i] <= lst[j]
  3.     #@ ensures result <-> exists i. 0 <= i < len(lst) and lst[i] == x
  4.     inf = 0
  5.     sup = len(lst)-1
  6.     while inf <= sup:
  7.         #@ variant sup - inf
  8.         #@ invariant 0 <= inf and sup < len(lst)
  9.         #@ invariant forall i. (0 <= i < inf -> lst[i] < x)
  10.         #@ invariant forall i. (sup < i < len(lst) -> lst[i] > x)
  11.         mid = (inf + sup)//2
  12.         if lst[mid] == x:
  13.             return True
  14.         elif lst[mid] < x:
  15.             inf = mid + 1
  16.         else:
  17.             sup = mid - 1
  18.     return False

Télécharger

Seule la preuve de terminaison est au programme. Cependant il est possible de formuler un invariant utilisant le fait que la liste est triée. La postcondition est que, puisque la fonction renvoie un booléen,

  • ce booléen est True s’il existe un indice i tel que l’élément cherché est dans le tableau, à cet indice,
  • le booléen est False si un tel indice n’existe pas (ce qui signifie que l’élément n’est pas dans le tableau)

L’invariant est qu’à tout instant l’indice auquel l’élément a des chances de se trouver est entre les bornes inférieure et supérieure, soit que

  • tous les éléments du tableau qui sont avant inf sont plus petits que l’élément cherché,
  • tous les éléments du tableau qui sont après sup sont supérieurs à l’élément cherché.

En ce qui concerne la partie qui est au programme, le variant le plus naturel est la longueur sup-inf de l’intervalle de recherche. On peut montrer que c’est un variant, parce qu’à chaque passage dans la boucle,

  • ou bien on augmente la borne inférieure,
  • ou bien on diminue la borne supérieure.

La longueur de l’intervalle est même divisée par 2 à chaque itération, ce qui rend l’algorithme très rapide.

Ainsi, l’outil why3 (version Python pour coller au programme) permet de mettre les élèves en autonomie relative : ils conjecturent un variant ou un invariant, puis le font tester par why3 avant d’appeler le professeur au secours. Ce genre d’activité, assez chronophage, présente les avantages suivants :

  • L’apprentissage des élèves est actif (ils ne se bornent pas à attendre la réponse du professeur).
  • On passe du temps sur les notions de variant et invariant, ce qui est nécessaire (ne serait-ce que parce que c’est au programme).
  • En commençant par des exemples simples, on peut pratiquer une pédagogie par répétition dans une progression spiralaire.
  • On peut même se contenter de pratiquer why3 sur des exemples simples seulement, et une fois que les notions de variant et invariant sont consolidées, aller vers un traitement moins formel de la question.
  • Les élèves apprécient de manipuler des outils professionnels, qui n’ont pas été créés juste à des fins pédagogiques.
  • why3 peut même être un sujet de projet...

Voir aussi

Le cours de Fred Mesnard en L3, et notamment les liens vers les tutoriels vidéo de Rustan Leino.


[1Et surtout, distinguer les variants des invariants, les deux noms se ressemblant.

[2La preuve peut être faite oralement au tableau (en vidéoprojetant why3) : comme à chaque passage dans la boucle, on récolte une graine, le nombre de graines dans la première case décroît au cours du temps.

[3Il remonte au moins à l’époque des pharaons...

[4Dans le programme, à propos des tableaux, il est dit « itérer sur les élements d’un tableau » mais aussi « lire [...] les éléments d’un tableau grâce à leurs index ». Les deux capacités sont attendues. C’est l’occasion de comparer les approches.

[5Cette propriété des entiers naturels est à l’origine de la notion de variant : pour un bon ordre tout ensemble non vide a un plus petit élément et c’est en particulier le cas pour l’ensembe des valeurs prises par le variant.

[6En activité débranchée, certains élèves font ainsi.

[7Mais c’est l’invariant qui est au programme, pas le variant...


Documents joints

PDF - 8.5 ko
PDF - 19.6 ko
Scalable Vector Graphics - 1.6 ko
Zip - 814 octets
Zip - 658 octets

Commentaires