Génie Logiciel
Introduction à la méthode B

Christine Paulin

Maîtrise 2001-2002

• Introduction
  • Objectifs du cours
  • Contexte et motivations
  • Applications
  • Plan du cours
• Les bases du langage de la méthode B
  • Les expressions
  • Les formules
  • Substitution élémentaire
  • Les relations et fonctions
  • Méthodes de preuve
• Machines abstraites
  • Introduction
  • Les substitutions
  • Structure d'une machine abstraite
  • Combiner des machines abstraites
• Raffinement
  • Introduction
  • Substitution et programme
  • Raffiner une substitution
  • Raffiner une machine abstraite
• Implantation
  • Principes
  • Restrictions
  • La clause IMPORTS
  • La clause VALUES
  • Substitution WHILE
  • Exemple
• Conclusion
• Eléments du langage de la méthode B
  • Opérations arithmétiques
  • Les ensembles
  • Les formules
  • Relations et fonctions
• Exemple : un carnet d'anniversaire
  • Modélisation
  • Machine défensive
  • Raffinement
  • Implantation
• Références
• Rappels sur la logique de Hoare
  • Conditionnelle
  • Affectation
  • Échange de valeurs
  • Boucle
• Langage de la méthode B
  • Formules
  • Objets et formules
  • Substitutions
• Machines
  • Signalisation

Ce document a été traduit de L^AT_EX par H^EV^EA et H^AC^HA.