Différences entre les versions de « Langage B »

10 octets ajoutés ,  il y a 8 ans
m
aucun résumé de modification
(wikification)
m
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éficibénéficie d'un prouveur. Il est donc possible d'énoncer des proriétépropriétés invarianteinvariantes sur l'ensemble du système quel que soit son état.
 
 
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,l'initialisation du système.
Les variables sont définidé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 fonctionfonctions de notre machine.
Une opération se déclare de la façon suivante:
<code>nomDeLOperation =
END</code>
 
Dans notre cas on peux voir que les deux variablevariables prennent chacunechacunes la valeur de l'autre. Ceci peux se faire en seulelemntseulement deux lignelignes, opération sur place, grâce au fait que les opérationopérations sont toutes en parallèle.
 
{{Autres projets|w=Méthode B|b=Programmation méthode B}}
3

modifications