Installation unique avec Docker
La méthode la plus simple pour utiliser why3 et Isabelle est d'utiliser un conteneur Docker à partir de l'image docker-cs3asl en utilisant ce script Linux ou ce script Windows
Utilisation de la version en ligne
Vous pouvez utiliser Why3 en ligne :
Mais vous ne pouvez pas choisir la version et ni utiliser Isabelle ou Coq pour faire des pruves.
Installations indépendantes des différents outils
Nous utiliserons Why3 version 1.4.0. Vous pouvez l'installer sur votre ordinateur avec opam
Nous utiliserons également Isabelle pour certaines preuves qui ne sont pas traitées par les prouveurs automatiques. Vous pouvez l'installer facilement sur votre ordinateur quel que soit son système d’exploitation.
Bonus
Vous pouvez utiliser Eclipse avec un plug-in qui permet d'éditer du code Micro C et d'exporter les annotations logiques vers Isabelle.
Pour installer ce plug-in dans Eclipse, allez dans le menu Help > Install New Software…, puis ajoutez le site de mise à jour en cliquant sur Add… et en donnant le nom Micro C feature update site et l'URL https://wdi.centralesupelec.fr/boulanger/misc/microc-update-site/. Il ne vous reste alors qu'à sélectionner ce site dans le menu, puis à cocher la case MicroCfeature pour poursuivre. Si vous avez le message There are no categorized items, il suffit de décocher la case Group items by category.
Vous aurez alors une option pour ouvrir un fichier C dans Why3 dans le menu Run As…, un item permettant d'exporter les définitions vers Isabelle dans le menu Acceleo Model to Text, et, pour les fichiers Isabelle, une option pour ouvrir le fichier dans Isabelle dans le menu Run As….
Pour ceux qui seraient intéressés, ce plug-in est une illustration de l'utilisation des notions vues dans mon cours d'ingénierie des modèles. Son code est disponible sur GitHub.