« Langage B » : différence entre les versions
mAucun résumé des modifications |
|||
| Ligne 17 : | Ligne 17 : | ||
== Première machine == |
== Première machine == |
||
La première machine que nous allons voir permet de décrire un programme qui permute la valeur de deux variable. |
La première machine que nous allons voir permet de décrire un programme qui permute la valeur de deux variable. |
||
< |
<source lang=C> |
||
MACHINE |
MACHINE |
||
swap |
swap |
||
| Ligne 34 : | Ligne 34 : | ||
END |
END |
||
END |
END |
||
</ |
</source> |
||
Comme vous pouvez le voir les machines sont composé de plusieurs |
Comme vous pouvez le voir les machines sont composé de plusieurs éléments. Le nom de la machine précédé du mot clef MACHINE(Tout les mot clef 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: |
Un Type se déclare donc de la manière suivante: |
||
<code language=B>nomDeVariable : TypeDeLaVariable</code> |
<code language=B>nomDeVariable : TypeDeLaVariable</code> |
||
| Ligne 46 : | Ligne 46 : | ||
Et finalement nous en arrivons à la partie OPERATION. C'est dans cette section que sont définit les fonctions de notre machine. |
Et finalement nous en arrivons à la partie OPERATION. C'est dans cette section que sont définit les fonctions de notre machine. |
||
Une opération se déclare de la façon suivante: |
Une opération se déclare de la façon suivante: |
||
< |
<source lang="C">nomDeLOperation = |
||
BEGIN |
BEGIN |
||
operation1||operation2 |
operation1||operation2 |
||
END</ |
END</source> |
||
Dans notre cas on peux voir que les deux variables prennent chacunes la valeur de l'autre. Ceci peux se faire en seulement deux lignes, opération sur place, grâce au fait que les opérations sont toutes en parallèle. |
Dans notre cas on peux voir que les deux variables prennent chacunes la valeur de l'autre. Ceci peux se faire en seulement deux lignes, opération sur place, grâce au fait que les opérations sont toutes en parallèle. |
||
Version du 22 mai 2013 à 00:05
|
Cette page doit être wikifiée, il est nécessaire de la mettre en forme et d'ajouter des liens internes vers d'autres leçons de Wikiversité. Votre aide est la bienvenue ! |
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 preuve sur le modèle ainsi défini. La platforme 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 à été utilisé pour divers projet d'envergure tel que la ligne 14 du métro parisien. Grâce au travaux effectué par Ericson sur ce projet le langage à pu progresser, ainsi que le prouveur.
Objectif de ce cours
Le but de ce cours est de permettre de comprendre la syntaxe et les particularités du langage B.
Vocabulaire
Une Machine : Un modèle de système écrit en B
Première machine
La première machine que nous allons voir permet de décrire un programme qui permute la valeur de deux variable.
MACHINE
swap
VARIABLES
xx, yy
INVARIANT
xx : NAT & yy : NAT
INITIALISATION
xx :: NAT ||
yy :: NAT
OPERATIONS
echange =
BEGIN
xx := yy
|| yy := xx
END
END
Comme vous pouvez le voir les machines sont composé de plusieurs éléments. Le nom de la machine précédé du mot clef MACHINE(Tout les mot clef 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:
nomDeVariable : TypeDeLaVariable
Dans notre cas il s'agit de variable de type NAT, pour naturel.
l'opérateur & permet de chainer les propriété 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ération nous utilisons l'opérateur ||. Cet opérateur défini que deux opération sont exécuté 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. Une opération se déclare de la façon suivante:
nomDeLOperation =
BEGIN
operation1||operation2
END
Dans notre cas on peux voir que les deux variables prennent chacunes la valeur de l'autre. Ceci peux se faire en seulement deux lignes, opération sur place, grâce au fait que les opérations sont toutes en parallèle.