Public visé

Toute personne ayant des notions de programmation et de logique et désirant comprendre ce que peut être la preuve d'un compilateur. Il faut notamment être à l'aise avec les notions de récursion et d'induction (en informatique ou en logique).

Cet atelier vous invite à pratiquer pour apprécier l'intérêt d'un outil de modélisation logique, mais il est tout à fait possible de profiter de l'atelier sans utiliser d'ordinateur, quitte à refaire la manip plus tard chez vous si cela éveille un intérêt.

Pour profiter pleinement de l'atelier et de son aspect « mains dans le cambouis », il est conseiller d'installer Isabelle/HOL sur votre ordinateur à l'avance et de vérifier qu'il se lance correctement grâce au code qui vous est donné plus bas sur cette page.

Introduction

On s'intéresse à des expressions arithmétiques simples sur les entiers. Pour simplifier encore plus le problème, on ne considère qu'une seule opération : l'addition.

On souhaite donc pouvoir représenter et évaluer des expressions du type {$2+3$}, ou {$5+(1+8)$}.

On considère maintenant une machine permettant de stocker des entiers sur une pile (opération PUSH), et disposant d'une instruction ADD qui prend les deux entiers au sommet de la pile et place leur somme sur la pile.

On peut donc transformer une expression arithmétique en une suite d'instructions pour la machine, c'est ce qu'on appelle compiler l'expression pour cette machine. Par exemple, l'expression {$2+3$} sera compilée en PUSH 2; PUSH 3; ADD.

Si tout est correct, évaluer une expression ou exécuter le programme obtenu en la compilant devrait donner le même résultat. C'est ce que nous allons démontrer.

Origine de cet exemple

Cet exemple est présenté dans une vidéo de la chaîne Youtube Computerphile.

Malheureusement, cette vidéo n'aborde pas la preuve formelle de correction et ne fait que tester que le résultat obtenu est correct sur quelques exemples.

Outillage

Pour modéliser les expressions et la machine d'exécution, nous allons utiliser Isabelle/HOL, un assistant de preuve disponible pour Mac, Windows et Linux.

Isabelle/HOL nous permet d'utiliser le {$\lambda$}-calcul typé et la logique d'ordre supérieur pour modéliser nos expressions et notre machine d'exécution, pour définir les fonctions d'évaluation, d'exécution et de compilation, et enfin pour prouver la correction du compilateur.

Déroulement de l'atelier

Nous commencerons par définir un type de donnée permettant de représenter les expressions, qui sont soit un entier, soit la somme de deux expressions.

Nous définirons ensuite une fonction d'évaluation qui prend en argument une expression et rend sa valeur.

Il faudra ensuite modéliser la machine à pile en définissant un type pour représenter les opérations PUSH et ADD, un programme étant simplement une liste d'opérations. L'état de la machine se réduit à une pile d'entiers que nous représenterons grâce à une liste. Il ne restera qu'à définir une fonction d'exécution qui prend en argument un programme et une pile et qui rend la pile résultant de l'exécution du programme.

Enfin, nous définirons une fonction de compilation, qui prend en argument une expression et qui rend un programme.

Pour finir, nous prouverons que la fonction de compilation est correcte. L'intérêt de cette étape n'est pas forcément de faire la preuve en Isabelle, mais plutôt de définir ce qu'est la correction, et de déterminer la structure de la preuve.

Le tout reste assez simple et tient en une quarantaine de lignes.

Contenu pour tester votre installation d'Isabelle/HOL

Après avoir lancé Isabelle, vous devriez avoir un fichier Scratch.thy ouvert dans l'éditeur. Si vous collez le texte suivant dans cette fenêtre :

theory Scratch

imports Main

begin

datatype money =
    Nothing
  | More money

term ‹More (More (More Nothing))›

fun earn
  where
    ‹earn Nothing = (0::nat)›
  | ‹earn (More h) = 1 + (earn h)›

value ‹earn (More (More (More Nothing)))›

theorem ‹earn (More m) > (earn m)›
  by simp

end

il ne devrait pas y avoir d'erreur, et vous devriez voir des informations dans la fenêtre Output quand vous placez le curseur après les différentes lignes (notamment après la définition de la fonction, après l'appel à value et après le théorème).

Si vous ne comprenez pas cet exemple, ce n'est pas grave, il est un peu idiot et ne sert qu'à tester qu'Isabelle fonctionne sur votre machine.

Solution

Version complète avec somme, différence, produit et quotient :

Présentation de l'enseignement en informatique à CentraleSupélec

https://wdi.centralesupelec.fr/boulanger/2023-06-09/PresInfoCS_2023-06-09.html