CentraleSupélec LMF, UMR CNRS 9021
Département informatique Laboratoire Méthodes Formelles
Bât Breguet, 3 rue Joliot-Curie Bât 650 Ada Lovelace, Université Paris Sud
91190 Gif-sur-Yvette, France Rue Noetzlin, 91190 Gif-sur-Yvette, France
Enseignement

Table des matières

Exemples de code, techniques de programmation Exemples

Des exemples montrant comment résoudre des problèmes récurrents en Java : lire et écrire dans un fichier, créer une interface graphique, sélectionner un fichier, lire et écrire un fichier XML etc.

Une page sur l'utilisation de Greenfoot avec ou sans Eclipse

Exemples et documentation pour le cours de troisième année Concepts des langages et techniques de programmation

Première année 1ère année

Algorithmique Algo

Les corrigés sont donnés dans le canal Teams des groupes de TD.

Troisième année 3ème année

Plug-in Eclipse pour MicroC (Isabelle/Why3)

MicroC update site: https://wdi.centralesupelec.fr/boulanger/misc/microc-update-site/

Ce plug-in Eclipse propose un éditeur de MicroC, la version de C supportée par Why3, ainsi que le langage d'annotation de programmes. Il contient également un plugin permettant d'exporter les lemmes et prédicats vers Isabelle afin de faire les preuves. Deux menus permettent d'ouvrir un fichier MicroC dans Why3 et une théorie Isabelle dans Isabelle/HOL.

Machines virtuelles et images DockerVMs & Docker

Pour le cours d'analyse statique

Je propose deux solutions de virtualisation pour les applications qui ne fonctionnent pas sur toutes les plateformes : un conteneur Docker et une machine virtuelle VirtualBox gérée par Vagrant.

Sous Linux, utilisez Docker, c'est ce qui donne les meilleures performances.

Sous Windows et MacOS, vous pouvez utiliser Docker ou Vagrant. Cette dernière solution est plus simple si la virtualisation (Hyper-V) n'est pas possible (version Home de Windows 10). Docker fonctionne maintenant sous Windows 10 Home en utilisant WSL2.

Les deux possibilités pour l'utilisation de why3 et de Soufflé :

Test

Pour tester votre machine, vous pouvez copier ce fichier dans le répertoire, puis dans le conteneur, exécuter : cd /workspace; why3 ide prog.mlw. L'utilisation de Tools > Provers > Alt-Ergo devrait suffire à prouver les obligations de preuve de ce programme.

Vous pouvez également faire le petit exemple Soufflé décrit sur https://souffle-lang.github.io/simple

Les fichiers sources pour l'image et la machine virtuelle sont disponibles sur https://github.com/Frederic-Boulanger-UPS/docker-3asl

Pour le cours de preuve

Voir cette page pour les différentes possibilités d'installation.