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

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

• Cours de principes de fonctionnement des ordinateurs
• Cours d'ingénierie dirigée par les modèles
• Cours de sémantique des langages

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.

Images Docker

Pour les cours d'ingénierie dirigée par les modèles, d'analyse statique, de logique, de sémantique des modèles, et de preuve, je propose une image Docker qui vous évite les problèmes d'installation et les procédures particulières liées aux différents systèmes d'exploitation.

Docker fonctionne maintenant sous Windows 10 Home en utilisant WSL2.

Cette image contient une installation d'Eclipse suffisante pour le cours d'ingénierie dirigée par les modèles, ainsi que Soufflé pour le cours d'analyse statique, Isabelle et Why3 pour le cours de sémantique, Isabelle, Coq et FramaC pour le cours de preuve.

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-cs3asl