CentraleSupélec LRI
Département informatique Équipe MODHEL
3 rue Joliot-Curie Bât 650 Ada Lovelace, Université Paris Sud
F-91192 Gif-sur-Yvette cedex, France Rue Noetzlin, 91190 Gif-sur-Yvette, France
Isabelle

Isabelle est un assistant de preuve.

Je l'utilise dans mon cours Sémantique des langages en majeure Systèmes informatiques.

Pour prouver la correction de l'algorithme d'Euclide (par soustractions successives), on utilise la définition suivante du PGCD :

Le pgcd de {$a$} et {$b$} est un diviseur commun de {$a$} et {$b$} tel que tout autre diviseur commun de {$a$} et {$b$} le divise.

Pour les entiers, on utilise habituellement une définition du PGCD fondé sur l'ordre :

Le pgcd de {$a$} et {$b$} est un diviseur commun de {$a$} et {$b$} tel que tout autre diviseur commun de {$a$} et {$b$} lui est inférieur.

L'équivalence de ces deux définitions peut être démontrée avec Isabelle.