Ce qui est à faire

Prouver en utilisant Isabelle, les programmes suivants :

1. Somme de 2 entiers n et m
2. Somme des n premiers entiers
3. Carré d'un nombre entier
4. Racine carrée entière d'un nombre
5. Minimum d'un tableau de nombres
6. Fibonacci ...
   

(Pour écrire certains invariants, il faudra utiliser certains opérateurs mathématiques comme $\sum$). Ces opérateurs sont définis dans les fichiers HOARE.thy et HOARE.ML . Pour utiliser ces opérateurs, charger ces fichiers sous votre répertoire, puis taper use_thy "HOARE";. Vous pouvez définir de nouveaux opérateurs en éditant ces fichiers)

Conseil: éditer un fichier .ML pour y écrire vos exemples et copier-coller dans l'interpréteur à partir de l'éditeur.