« Langage B » : différence entre les versions

Contenu supprimé Contenu ajouté
Floco99 (discussion | contributions)
m orthographe
Ligne 2 :
 
Le langage B est issu de la Méthode B. Ce langage a été défini initialement par JR-Abrial. Il s'agit d'un langage formel qui permet d'exprimer des modèles conceptuels.
L'intérêt de ce langage est de permettre d'établir des preuvepreuves sur le modèle ainsi défini.
La platformeplateforme B bénéficie d'un prouveur. Il est donc possible d'énoncer des propriétés invariantes sur l'ensemble du système quel que soit son état.
 
 
== Utilisation du langage B ==
Le B àa été utilisé pour divers projetprojets d'envergure tel que la ligne 14 du métro parisien. Grâce auaux travaux effectuéeffectués par Ericson sur ce projet le langage àa pu progresser, ainsi que le prouveur.
 
== Objectif de ce cours ==
Ligne 16 :
 
== Première machine ==
La première machine que nous allons voir permet de décrire un programme qui permute la valeur de deux variablevariables.
<source lang=C>
MACHINE
Ligne 35 :
END
</source>
Comme vous pouvez le voir les machines sont composécomposées de plusieurs éléments. Le nom de la machine précédé du mot clef MACHINE (ToutTous les motmots clefclefs doivent être écrit en majuscule). Ensuite le nom de la machine. Ensuite arrivent les variables de la machine. C'est l'unique façon en B de déclarer une variable. À ce stade la variable n'est pas typée encore. Le typage se fait dans la partie INVARIANT. Dans cette partie se déclarent toutes les propriétés qui doivent être vérifiable en tout point du programme.
Un Type se déclare donc de la manière suivante:
<code language=B>nomDeVariable : TypeDeLaVariable</code>
Dans notre cas il s'agit de variable de type NAT, pour naturel.
l'opérateur & permet de chainer les propriétépropriétés entre elles.
Ensuite vient l'initialisation du système.
Les variables sont définies par n'importe quelle valeur de type Naturel.
Ici pour chainer les opérationopérations nous utilisons l'opérateur ||. Cet opérateur défini que deux opérationopérations sont exécutéexécutées en parallèle. En effet en B toute opération doit être effectué en parallèle.
 
Et finalement nous en arrivons à la partie OPERATION. C'est dans cette section que sont définit les fonctions de notre machine.
Ligne 51 :
END</source>
 
Dans notre cas on peuxpeut voir que les deux variables prennent chacuneschacune la valeur de l'autre. Ceci peuxpeut se faire en seulement deux lignes, opération sur place, grâce au fait que les opérations sont toutes en parallèle.
 
{{Autres projets|w=Méthode B|b=Programmation méthode B}}