Méthode B/Introduction

Selon J.R. Abrial, auteur de B, B est :

• une méthode
• une théorie
• un langage (le langage des substitutions généralisées)
• un ensemble d'outils (Atelier B, btoolkit, projet Rodin ([1]))

"B est une méthode pour spécifier, concevoir et coder des systèmes logiciels" (J.R. Abrial in The B Book, page XV)

• Couverture : spécifications techniques, conception par étapes de raffinage successives, architecture en couches, génération de code exécutable
• Preuves : Le développement est assisté par la preuve des opérations (on prouve que si on appelle une opération sous sa précondition, l'invariant de la machine est préservé), et par la preuve du raffinage
• Machines abstraites : une telle machine encapsule les données qui ne sont accessibles que via les opérations. Les données sont spécifiées avec les concepts mathématiques d'ensembles, relations, fonctions, suites, arbres dans un invariant (en ce qui concerne les variables), dans des propriétés (en ce qui concerne les constantes). Les opérations sont spécifiées comme des substitutions (ex : x := x + 1, qui se lit "x devient égal à x + 1"). Une substitution peut être préconditionnée, gardée, indéterministe. Dans une machine abstraite, il est interdit d'utiliser le séquencement (;). Les substitutions sont composées en parallèle (ex. : a := b || b := a).
• Le raffinage consiste à affaiblir les préconditions (jusqu'à les faire disparaître), réduire l'indéterminisme (qui aura disparu des machines d'implémentation), introduire le séquencement et la boucle.
• Trois types de machines : les machines abstraites (MACHINE), les raffinages (REFINEMENT), les machines traduisibles directement en code exécutable, écrire en pseudo-code Pascal (IMPLEMENTATION)
• Composition de machines : on peut composer des machines avec SEES, INCLUDES, USES, IMPORTS. Par exemple, une machine A qui inclut une machine B, n'a pas dans son répertoire d'opérations les opérations de A et de B. Mais les opérations de A peuvent dans leur définition faire appel aux opérations de B. Ainsi l'encapsulation est bien respectée.