ACTIONS
L'ordinateur à la rescousse
Un exemple de
démon s trateur
automatique est
le logiciel AltErgo , développé
par des chercheurs
de l 'U nivers ité
Paris Sud depui s
2007. Dan s la
sy ntax e d ' AltErgo, on peut énoncer que (la parti e
entière de) la moyenne de deux entiers
relatifs est toujours comprise entre ces
deux entiers avec la sy ntaxe suivante :
goal thm2: forall x, y: int.
X<= y ·>X<= (x+y)/2 <= y
li ne faut que quelques centièmes de
seconde à Alt-Ergo pour démontrer un
tel énoncé.
De nombreux démonstrateurs automatiques sont développés de par le monde
depuis plus d'un demi siècle. En 1996 ,
une conjecture de la théorie des groupes
qui résistait aux mathématiciens depui s
1933 a été prouvée par le démonstrateur automatique EQP, après huit jours
de calcul.
La preuue de programmes
Troisième outil : il est possible de faire
la preuve qu ' un progra mme informatique est correct, c'est-à-dire qu ' il fait
bien ce qu ' il est censé faire, en exprimant
cela comme un énoncé mathématique .
Plus précisément, un outil prend en entrée
un programme, ainsi qu 'une propriété que
ce programme doit vérifier, et produit en
sortie un ensemble d 'énoncés mathématiques qui , s'ils sont prouvés , garantissent la correction* du programme .
C'est notamment là que la démonstration ass istée par ordinateur, dan s les
deux acceptions précédentes , prend tout
son sens , car de telles preuves peuvent
être gigantesques et sont en général
* Le fait d'être correct. extrêmement fastidieuses .
Un exemple significatif de preuve de
programme est celui de la preuve d ' un
compil ateur C , réali sée en 2008 par un
chercheur d ' lnria (vo ir http ://compcert.inria.fr). Un autre exemple est celui
de la preuve d ' une parti e du logic iel de
la li g ne 14 du métro parisien , par la
société Matra en 1998.
Un des outils les plus utili sés en France
de preuve de programmes est le logiciel Wh y3 , développé à l' Université
Pari s Sud depuis 200 1. Il peut être utili sé conjointement avec de nombreux
ass istants de pre uve , dont Coq, et de
nombreux démonstrateurs automatiques ,
dont Alt-Ergo.
Considérons le programme expo figurant dans l'encadré ci-dessous et utiliso ns un log ici e l co mme Wh y3 pour
montrer que ce progra mme é lève bien
x à la puissance n .
On commence par énoncer précisément
la propriété que l'on souhaite vérifier. On
appe lle cela spécifier le programme.
Comme il s' agit ici d' une fonction , cette
spéc ification a deux composantes : une
propriété attendue à l'entrée de la fonction , appelée pré-condition , et une propriété attendue à la sortie de la fonction ,
appelée post-condition. Ici la pré-condition stipule que n ~ 0 et la post-condition que le résultat est égal à .i'. L'ensemble
de la pré-condition et de la post-condition forme ce que l'on appelle le contrat
de la fonction.
Même si cet exemple est très simple , la
spéc ification est une étape importante
et parfois diffic ile. En particulier, le lecteur doit pouvoir se persuader que c 'est
bie n là la propriété que l'on sou haite
pour le progra mme. Une e rre ur peut
facilement se g li sser dans l' énoncé et
la machine ne nous aidera pas.
On passe alors à l'étape de preuve . À
ce stade , il faut a ider l'outil Why 3 en
lui donnant une indication , sous la forme
Tangente Hors-série n°52. Mathématiques & informatique
L'ordinateur à la rescousse
Un exemple de
démon s trateur
automatique est
le logiciel AltErgo , développé
par des chercheurs
de l 'U nivers ité
Paris Sud depui s
2007. Dan s la
sy ntax e d ' AltErgo, on peut énoncer que (la parti e
entière de) la moyenne de deux entiers
relatifs est toujours comprise entre ces
deux entiers avec la sy ntaxe suivante :
goal thm2: forall x, y: int.
X<= y ·>X<= (x+y)/2 <= y
li ne faut que quelques centièmes de
seconde à Alt-Ergo pour démontrer un
tel énoncé.
De nombreux démonstrateurs automatiques sont développés de par le monde
depuis plus d'un demi siècle. En 1996 ,
une conjecture de la théorie des groupes
qui résistait aux mathématiciens depui s
1933 a été prouvée par le démonstrateur automatique EQP, après huit jours
de calcul.
La preuue de programmes
Troisième outil : il est possible de faire
la preuve qu ' un progra mme informatique est correct, c'est-à-dire qu ' il fait
bien ce qu ' il est censé faire, en exprimant
cela comme un énoncé mathématique .
Plus précisément, un outil prend en entrée
un programme, ainsi qu 'une propriété que
ce programme doit vérifier, et produit en
sortie un ensemble d 'énoncés mathématiques qui , s'ils sont prouvés , garantissent la correction* du programme .
C'est notamment là que la démonstration ass istée par ordinateur, dan s les
deux acceptions précédentes , prend tout
son sens , car de telles preuves peuvent
être gigantesques et sont en général
* Le fait d'être correct. extrêmement fastidieuses .
Un exemple significatif de preuve de
programme est celui de la preuve d ' un
compil ateur C , réali sée en 2008 par un
chercheur d ' lnria (vo ir http ://compcert.inria.fr). Un autre exemple est celui
de la preuve d ' une parti e du logic iel de
la li g ne 14 du métro parisien , par la
société Matra en 1998.
Un des outils les plus utili sés en France
de preuve de programmes est le logiciel Wh y3 , développé à l' Université
Pari s Sud depuis 200 1. Il peut être utili sé conjointement avec de nombreux
ass istants de pre uve , dont Coq, et de
nombreux démonstrateurs automatiques ,
dont Alt-Ergo.
Considérons le programme expo figurant dans l'encadré ci-dessous et utiliso ns un log ici e l co mme Wh y3 pour
montrer que ce progra mme é lève bien
x à la puissance n .
On commence par énoncer précisément
la propriété que l'on souhaite vérifier. On
appe lle cela spécifier le programme.
Comme il s' agit ici d' une fonction , cette
spéc ification a deux composantes : une
propriété attendue à l'entrée de la fonction , appelée pré-condition , et une propriété attendue à la sortie de la fonction ,
appelée post-condition. Ici la pré-condition stipule que n ~ 0 et la post-condition que le résultat est égal à .i'. L'ensemble
de la pré-condition et de la post-condition forme ce que l'on appelle le contrat
de la fonction.
Même si cet exemple est très simple , la
spéc ification est une étape importante
et parfois diffic ile. En particulier, le lecteur doit pouvoir se persuader que c 'est
bie n là la propriété que l'on sou haite
pour le progra mme. Une e rre ur peut
facilement se g li sser dans l' énoncé et
la machine ne nous aidera pas.
On passe alors à l'étape de preuve . À
ce stade , il faut a ider l'outil Why 3 en
lui donnant une indication , sous la forme
Tangente Hors-série n°52. Mathématiques & informatique