La MÉTHODE B : est avant tout destinée à produire un code à fort niveau de confiance, au terme d’un cycle de développement mêlant formalisme et preuve mathématique. L’approche utilisée consiste à éviter d’introduire des erreurs au cours du développement grâce à la preuve, plutôt qu’à utiliser des tests pour les découvrir vers la fin du développement.
Le code produit est issu de la traduction des implémentations écrites dans le langage B0, sous-ensemble du langage B et d’une syntaxe proche d’un quelconque langage structuré. La phase de traduction permet alors de produire un code cible de forme similaire à celle du modèle B0.
Cette traduction dite « 1 pour 1 » permet le cas échéant de vérifier facilement le code en sortie du générateur par comparaison avec le modèle B0.
