4.2.1.5 Les règles de cohérences sous
forme d'OCL (.chk)
Nous avons établi des propriétés
décrivant des contraintes d'utilisation d'Event-B. De telles
propriétés sont décrites d'une façon informelle et
formelle en se servant d'OCL. ~ Le cas d'ERROR
Tous les contextes attachés à un ROOT doivent
avoir des noms deux à deux différents. Une formalisation
partielle de cette propriété en OCL est :
page 58
4.2 Les méta-modèles de notre approche
|
context Machine ERROR
"Le nom de variable doit etre unique":
variables.forAll(var1| variables.notExists(var2|var1!=var2
var1.name==var2.name));
|
En cas d'erreur un message sera affiché et
l'exécution sera arrêtée. Ceci est illustré par la
Figure 4.8 suivante :
FIGURE 4.8 - Cas d'erreur
~ Le cas de WARNING
Le nom de la machine doit commencer avec une majuscule. Ceci est
formalisé en OCL comme suit :
|
context Machine WARNING
"le nom doit etre commencer par majuscule" :
Machine.name.startsWith("M");
|
Le type de contrainte « WARNING » n'arrête pas le
workflow, il affiche seulement un message. Ceci est illustré par la
Figure 4.9 suivante :
page 59
4.2 Les méta-modèles de notre approche
FIGURE 4.9 - Cas de warning
L'annexe A présente le reste des contraintes « OCL
».
| 
