Paraphrase d'une spécification formelle B, un premier essai.

Cet article decrit une tentative de paraphrasage d'une specification B, paraphrasage devant permettre a un utilisateur, peu au fait du langage utilise, de valider neanmoins celle-ci. Ceci est possible grâce a la production d'un texte en langue naturelle paraphrasant la specification B Seule la partie statique des donnees d'une machine est prise en compte dans cette tentative. La specification est supposee, en outre, etre redigee selon ce que nous appelons un « style de base ». Nous pensons qu'il ne peut y avoir de veritable validation par l'utilisateur d'une specification B que si celle-ci est « traduite » en francais. Cette « traduction », ce paraphrasage, a deja fait l'objet de plusieurs propositions que nous rappelons. Nous prenons appui sur celles-ci pour definir les regles qui nous permettent de passer d'une specification B a des structures profondes, puis a des structures de surface et, enfin, a des phrases L'article se termine par un bilan de cet essai et une evocation des travaux de recherche a entreprendre, en vue d'ameliorer la qualite du texte produit et d'etendre les mecanismes proposes a tout le langage B