Conclusion et perspectives
D
ans ce mémoire, nous avons abordé la
problématique de développement des logiciels et systèmes
complexes sensibles aux erreurs. Pour éviter les erreurs
inhérentes au développement de ces logiciels et systèmes,
nous avons proposé une approche IDM permettant de transformer une
modélisation semi-formelle ECore vers une spécification formelle
Event-B, qui permet d'obtenir une spécification cohérente et
digne de confiance du futur système en utilisant les outils
associés à Event-B : générateur d'obligations de
preuves, prouveur automatique et interactif, animateur et model-checker.
Pour y parvenir, nous avons élaboré deux
méta-modèles : le méta-modèle ECore qui joue le
rôle de méta-modèle source dans notre approche IDM de
transformation d'une modélisation décrite en ECore vers une
spécification en Event-B. Et le méta-modèle Event-B qui
joue le rôle de méta-modèle cible. De plus, nous avons
conçu et réalisé un programme ECore2Event-B.atl permettant
de transformer un modèle source ECore conforme au
méta-modèle ECore vers un modèle cible Event-B conforme au
méta-modèle Event-B en respectant des contraintes
exprimées en OCLinECore et en utilisant un langage déclaratif ATL
comme langage de transformation M2M. Notre programme ECore2Event-B.atl est
purement déclaratif et utilise avec profit les constructions
déclaratives fournis par ATL : telles que helpers (attribut,
opération), règles standard, règles paresseuses. En outre,
nous avons proposé une transformation du modèle Event-B vers
texte Event-B en respectant des contraintes exprimées en Check et en
utilisant l'outil Xpand qui nous a permis de transformer un modèle
Event-B vers code moyennant l'écriture des templates Xpand.
Quant aux perspectives de ce travail, nous pourrions envisager
les prolongements suivants:
1. Enrichir notre méta-modèle Event-B on ajoutant
d'autres concepts et d'autres propriétés décrivant des
contraintes d'utilisation des constructions Event-B.
Conclusion et perspectives
2. Améliorer notre programme ECore2Event-B.atl par de
helpers (opération).
3. Proposer l'opération de transformation inverse
d'Event-B vers ECore.
page 93
94
Appendices
95
A Les règles de cohérence du méta-
modèle Event-B sous forme d'OCL
(.chk)
|
1 import ecore ;
3 /* Contrainte attach EPackage */
context EPackage ERROR
5 " UniqueClassifierNames " :
e C l a s s i f i e r s . forAll ( a1| e C l a s s i f i e r s .
notExists ( a2 | a1!=a2 && a1 . name==a2 . name)) ;
7 context EPackage ERROR
" UniqueSubpackageNames " :
9 eSubpackages . forAll ( a1 | eSubpackages .
notExists ( a2 | a1!=a2 && a1 . name==a2 . name) ) ;
context EPackage ERROR
11 " WellFormedNsURI " :
nsURI!= null;
13
context EPackage ERROR
15 " WellFormedNsPrefixI " :
this . nsURI> 0;
17 /*Contrainte attach EClass */
context EClass ERROR
19 " UniqueOperationSignatures " :
eOperations . forAll ( a1 | eOperations . notExists ( a2 | a1!=a2
&& a1 . name==a2 . name));
21 /* context EClass ERROR
" noAttributesInInterface " :
23 i f ( this . interface==true ) then
eAttributes==0 ; :
25 context EClass ERROR
|
27
29
31
33
35 37 39 41 43 45 47 49
page 96
" CheckNamesEClass " :
eStructuralFeatures ->c o l l e c t ( self.
eStructuralFeatures ->c o l l e c t (name))->
excludesAll ( self. eOperations->c o l l e c t ( self.
eOperations->c o l l e c t (name))) ;
context EClass ERROR
" UniqueFeatureNames " :
eStructuralFeatures . forAll ( a1 | eStructuralFeatures .
notExists ( a2 | a1!=a2 && a1 .
name==a2 . name));
/* Contrainte attach abstract class EClassifier */
context EClassifier ERROR
" UniqueTypeParameterNames " :
eTypeParameters . forAll ( a1 | eTypeParameters . notExists ( a2
| a1!=a2 && a1 . name==a2 .
name));
context EClassifier ERROR
" WellFormedInstanceTypeName " :
this . name > 0;
/* Contrainte attach abstract class ENamedElement */
context ENamedElement ERROR
" WellFormedName " :
this . name>0;
/* Contrainte attach EAnnotation
context EAnnotation ERROR
" WellFormedName " :
this . name!= null; */
/* Contrainte attach abstract class ETypedElement */
context ETypedElement ERROR
" ValidLowerBound " :
lowerBound!=0 implies lowerBound >0 ;
51 context ETypedElement ERROR
" ValidUpperBound " :
55
57
53 upperBound!=0 implies ( lowerBound == 1
&& upperBound == -1) ;
/* Contrainte attach EEnum */
context EEnum ERROR
" UniqueEnumeratorNames " :
eLiterals . forAll ( a1 | eLiterals . notExists ( a2 | a1!=a2
&& a1 . name==a2 . name) ) ;
59
61
/* Contrainte attach EOperation */ context EOperation ERROR
|
|
|
|
|
|
|
|
uniqueTypeNames :
|
|
|
63
|
|
eTypeParameters . forAll ( a1 | eTypeParameters . notExists ( a2
| a1!=a2 && a1 . name==a2 . name));
|
|
|
65 context EOperation ERROR
UniqueParameterNames :
67 eParameters . forAll ( a1| eParameters .
notExists ( a2 | a1!=a2 && a1 . name==a2 . name)) ;
|
|
|
|
|
Checks.chk
|
|
page 97
98
B Les règles de cohérence du
méta-
modèle ECore sous forme d'OCLi-
2
4
6
8
10
12
14
16
nECore
P r o p r i t 1 :
Les m ta-attributs nsURI et nsPrefix de la m ta-classe EPackage
doit stocker
un identificateur valide qui doit tre non vide. Ceci peut
tre
f o r m a l i s en OCL comme suit :
invariant WellFormedNsURI :
nsURI . size () > 0;
invariant WellFormedNsPrefix : nsURI . size () > 0;
P r o p r i t 2 :
Tous les EClassifier ( EClass , EDataType ,EEnum) attach s un
EPackage doivent
avoir des noms deux deux d i f f rents . Ceci peut tre f o r m a
l i s en
OCL comme suit :
invariant UniqueClassifierNames :
eClassifier s ->forAll (a : EClassifier , b : EClassifier a .
name = b . name
implies a = b) ;
P r o p r i t 3 :
Un EPackage doit avoir un nom unique. Ceci peut tre f o r m a l i
s en OCL comme suit :
invariant UniqueSubpackageNames :
eSubpackages->forAll ( r1 : EPackage , r2 : EPackage r1
<> r2 implies r1 . name
<> r2 . name) ;
P r o p r i t 4 :
Une interface est une classe sans attribut. Ceci peut tre f o r m
a l i s en OCL
comme suit :
invariant noAttributesInInterface :
18
20
22 24 26 28
30 32 34 36 38
40
42
page 99
eAttributes->isEmpty () ;
P r o p r i t 5 :
Tous les EOperation attach s un EClass doivent avoir des
signatures deux
deux d i f f rents . Ceci peut tre f o r m a l i s en OCL comme
suit :
invariant UniqueOperationSignatures :
eOperations->forAll (a : EOperation , b : EOperation a . name
= b . name implies a
= b) ;
P r o p r i t 6 :
Toutes les Features ( EAttribute , EReference ) attach e s un
EClass doivent
avoir des noms deux deux d i f f rents .
Une formalisation partielle de cette p r o p r i t en OCL est:
invariant UniqueFeatureNames :
eStructuralFeatures ->forAll (a : EStructuralFeature , b :
EStructuralFeature a
. name = b . name implies a = b) ;
P r o p r i t 7 :
Dans un m me EClass une EOperation , un EAttribute et une
EReference doivent
avoir des noms deux deux d i f f rents . Ceci, est f o r m a l i
s en OCL comme
suit :
invariant CheckNamesEClass :
eStructuralFeatures ->c o l l e c t ( self.
eStructuralFeatures ->c o l l e c t (name))-> excludesAll ( self.
eOperations->c o l l e c t ( self. eOperations->c o l l e c t (name)))
;
P r o p r i t 8 :
Un param tre attach un EOperation doit avoir un nom et type
unique. Ceci
, est f o r m a l i s en OCL comme suit :
invariant UniqueParameterNames :
eParameters->forAll ( a1 : EParameter , a2 : EParameter a1
<> a2 implies a1 .
name <> a2 . name) ;
invariant UniqueTypeParameterNames :
eTypeParameters->forAll ( t1 : ETypeParameter , t2 :
ETypeParameter t1 <> t2
implies t1 . name <> t2 . name) ;
P r o p r i t 9 :
Le m ta-attribut name de la m ta-classe abstrait ENamedElement
doit
stocker un identificateur valide qui doit tre non vide. Ceci peut
tre
f o r m a l i s en OCL comme suit :
invariant WellFormedName : this . name . size () <> 0;
P r o p r i t 10 :
Un EEnum doit avoir un nom unique. Ceci peut tre f o r m a l i s
en OCL comme suit :
44
46
48
50
52
54
56
58
invariant UniqueEnumeratorNames :
eClassifier s ->forAll (a : EEnum, b : EEnum a . name = b .
name implies a = b) ;
P r o p r i t 11 :
Tous les EEnumLiteral attach s un composant doivent avoir des
noms deux
deux d i f f rents . Ceci peut tre f o r m a l i s en OCL comme
suit :
invariant UniqueEnumeratorLiterals ;
eLiterals ->forAll (a : EEnumLiteral , b : EEnumLiteral a .
name = b . name implies
a = b) ;
P r o p r i t 12 :
Le m ta-attribut source de la m ta-classe abstrait EAnnotation
doit
stocker un identificateur valide qui doit tre non vide. Ceci
peut tre
f o r m a l i s en OCL comme suit :
invariant WellFormedSourceURI : name. size () > 0;
P r o p r i t 13 :
Le m ta-attribut LowerBound de la m ta-classe abstrait
ETypedElement
doit stocker un identificateur valide qui doit tre e 0 ou 1 .
Et Le m ta-attribut UpperBound doit tre -1 ou 1 . Ceci
peut
tre f o r m a l i s en OCL comme suit :
invariant ValidlowerBoundd :
this . lowerBound = 0 or lowerBound = 1; invariant
ValidUpperBoundd :
this . upperBound = - 1 or lowerBound = 1;
page 100
101
C Les règles de transformation M2M
(Ecore2EventB.atl)
|
-- @path MM=/ecoree /metaModels/ ecore . ecore
2 -- @path MM1=/ecoree /metaModels/EventB .
ecore
4 module aaa ;
create OUT : MM1 from IN : MM;
6 helper context MM! EReference def :
getExtendedName () : String =
i f s e l f . changeable=f a l s e then
8 ' '
else
10 s e l f . name
endif ;
12 helper context MM! EReference def :
getERefernceName () : String =
i f ( s e l f . changeable=f a l s e ) and ( s e l f . v o l a t
i l e=true ) then
14 s e l f . name
else
16 OclUndefined
endif ;
18 helper context String def : firsttoUpper () :
String =
s e l f . substring (1 , s e l f . size ( ) ) . toLower () ;
20 helper context String def : firstToLower () :
String =
self. substring (1 , self. size () ) . toUpper () ;
22 helper def : GetEEnumLiteral1 : Sequence (MM!
EEnumLiteral ) =
MM! EEnumLiteral . allInstances ( ) ->
24 sortedBy ( e e . name) ;
helper def : GetEEnumLiteral2 : Sequence (MM! EEnumLiteral ) =
26 MM! EEnumLiteral . allInstances ( ) ->
sortedBy ( e e . name) ;
28 helper def : GetEClass1 : Sequence (MM!
EClass ) =
|
page 102
30
32
34
36
38
40
42
44
46
48
50
52
54
56
58
60
62
64
66
MM! EClass allInstances ( ) ->
sortedBy ( e e name) ;
helper def : GetEClass2 : Sequence (MM! EClass ) =
MM! EClass allInstances ( ) ->
sortedBy ( e e name) ;
helper def : GetEEnum : Sequence (MM!EEnum) =
MM!EEnum allInstances ( ) ->
sortedBy ( e e name) ;
helper def : GetEClass3 : Sequence (MM! EClass ) =
MM! EClass allInstances ( ) ->
sortedBy ( e e name) ;
helper def : GetEEnum1 : Sequence (MM!EEnum) =
MM!EEnum allInstances ( ) ->
sortedBy ( e e name) ;
helper def : GetEEnum2 : Sequence (MM!EEnum) =
MM!EEnum allInstances ( ) ->
sortedBy ( e e name) ;
helper def : GetEAttribute : Sequence (MM! EAttribute ) =
MM! EAttribute allInstances ( ) ->
sortedBy ( e e name) ;
helper def : GetEAttribute1 : Sequence (MM! EAttribute ) =
MM! EAttribute allInstances ( ) ->
sortedBy ( e e name) ;
helper def : GetEattribute : Sequence (MM! EAttribute ) =
MM! EAttribute allInstances ( ) ->
sortedBy ( e e name) ;
helper def : GetEReference2 : Sequence (MM! EReference ) =
MM! EReference allInstances ( ) ->
sortedBy ( e e name) ;
helper def : GetEReference3 : Sequence (MM! EReference ) =
MM! EReference allInstances ( ) ->
sortedBy ( e e name) ;
helper def : GetERef : Sequence (MM! EReference ) =
MM! EReference allInstances ( ) ->
sortedBy ( e e name) ;
helper def : GetEvent : Sequence (MM! EOperation ) =
MM! EOperation allInstances ( ) ->
sortedBy ( e e name) ;
helper def : GetEParameter : Sequence (MM! EParameter ) =
68
MM! EParameter . allInstances ( ) -> sortedBy ( e | e . name)
;
70
72
74
82
(
rule EPackage2RootContextMachine
{
76
from z :MM! EPackage
to
78
a :MM1!ROOT (
80
contextes <-Sequence {ctx } , contextes <-Sequence {mch}
) ,
ctx : MM1! Context
84
name <- z . name+' ctx ' ,
86
sets <-z . eClassifiers ->s e l e c t ( el | el .
oclIsTypeOf (MM! EClass ) ) ,
sets <-z . eClassifiers ->s e l e c t ( el | el .
oclIsTypeOf (MM!EEnum) ) ,
constants <- Sequence {thisModule . GetEEnumLiteral1->c o l
l e c t ( e | thisModule .
resolveTemp (e , ' const1 ')) } ,
axioms <- Sequence {thisModule. GetEEnumLiteral2->c o l l e
c t ( e | thisModule .
resolveTemp (e , ' const2 ')) }
88
90
92
page 103
) ,
94
mch : MM1! Machine
(
name <- z.name+'M',
variables <-Sequence {thisModule . GetEClass1->c o l l e c
t ( e | thisModule .
96
resolveTemp (e , ' const4 ')) } ,
variables <-Sequence {thisModule .GetEEnum->c o l l e c t (
e | thisModule . resolveTemp (
e,'enum'))},
98
variables <-Sequence {thisModule . GetEAttribute->c o l l e
c t ( e | thisModule.
resolveTemp (e , 'A')) } ,
variables <-Sequence {thisModule . GetEReference3->c o l l
e c t ( e | thisModule.
resolveTemp (e , ' s ')) } ,
invariants <-Sequence {thisModule . GetEClass2->c o l l e c
t ( e | thisModule .
resolveTemp (e , ' inv ')) } ,
100 102 104 106
invariants <-Sequence {thisModule .GetEEnum1->c o l l e c t
( e | thisModule . resolveTemp (e , ' inv1 ')) } ,
invariants <-Sequence {thisModule . GetEAttribute1->c o
l l e c t ( e | thisModule. resolveTemp (e , 'B')) } ,
invariants <-Sequence {thisModule . GetEReference2->c o
l l e c t ( e | thisModule. resolveTemp (e , ' ss ') ) } ,
events <-Sequence {thisModule. GetEClass3->c o l l e c t
( e | thisModule . resolveTemp (e ,'init'))},
events <-Sequence {thisModule . GetEEnum2->c o l l e c t
( e | thisModule . resolveTemp (e , ' init1 ' ) ) } ,
events <-Sequence {thisModule. GetEattribute->c o l l e c t
( e | thisModule . resolveTemp (e , ' init2 ')) } ,
events <-Sequence {thisModule . GetERef->c o l l e c t ( e
| thisModule . resolveTemp (e,' sss'))},
events <-Sequence {thisModule . GetEvent->c o l l e c t
( e | thisModule . resolveTemp (e , ' evt'))}
108 ) }
|
110
116
|
rule EClass2Sets { from
) ,
|
|
|
112
cc : MM! EClass
to
114
const3 : MM1! Sets (
name <- cc . name. firstToLower ()
118
const4 : MM1! Variable (
name <- cc . instanceClassName
120
) ,
inv : MM1! Invariant ( name <- ' inv0 ' ,
122
predicat <-cc . instanceClassName+' '+' Subset '+' '+cc .
name ) ,
124
126
i n i t :MM1! Event ( name <- 'INITIALISATION ' , actions
<-Sequence{ action2 }
128
page 104
) ,
130
action2: MM1! Action (
132
136 138 140 142 144 146 148 150 152 154
156 158 160 162 164 166
name <-' act ',
predicat <-cc . instanceClassName+' := '+' isEmpty () '
)
134 }
rule EEnum2Sets { from
Enum: MM!EEnum
to
sets: MM1! Sets ( name <- Enum. name
)
}
rule EEnumLiteral2ConstantsAndAxioms {
from
to
EnumLiteral : MM! EEnumLiteral
const1 : MM1! Constants (
name <- EnumLiteral . name
) ,
const2 :MM1! Axioms (
name <- 'axm1_2 ',
predicat <-'PARTITION'+' '+' ( '+EnumLiteral .eEnum. name+',
'+'{ '+
EnumLiteral . name+' } '+' ) '
)
}
rule EAttribute2Variable {
from
a : MM! EAttribute (a . changeable=true )
to
A: MM1! Variable (
page 105
name <-a . name
) ,
B: MM1! Invariant (
name <-' inv ' ,
predicat <-i f a . v o l a t i l e=true and a . unique=true
then
a . name+' '+'IN '+' '+' PartialInjective '+' ( '+ a .
eContainingClass .
instanceClassName+' , '+a . eAttributeType . name+' ) '
168
else i f a . v o l a t i l e=true and a . unique=f a l s e
then
a . name+' '+'IN '+' '+' PartialFunction '+' ( '+ a .
eContainingClass .
instanceClassName+' , '+a . eAttributeType . name+' ) '
170
else i f a . v o l a t i l e=f a l s e and a . unique=true
then
a . name+' '+'IN '+' '+' TotalBijective '+' ( '+ a .
eContainingClass .
instanceClassName+' , '+a . eAttributeType . name+' ) '
172
else
a . name+' '+'IN '+' '+' TotalFunction '+' ( '+ a .
eContainingClass .
instanceClassName+' , '+a . eAttributeType . name+' ) '
174
endif endif
176
endif
) ,
178
init2 :MM1! Event (
180
name <- 'INITIALISATION' , actions <-Sequence{ action3 }
182
) ,
action3 : MM1! Action (
184
name <-' act ',
predicat <-a . name+':= '+' isEmpty () '
186
)
}
188
190
page 106
rule EReference2Variable {
from
192
u : MM! EReference (u . changeable=true )
to
194
s : MM1! Variable (
name <- u . getExtendedName ()
196
) ,
ss : MM1! Invariant (
198
name <-' inv1_1 ',
predicat <-i f ( u . changeable=true and u . lowerBound=0 and
u . upperBound
=-1)and(u . eOpposite . lowerBound=0 and u . eOpposite .
upperBound=-1) then
200
u . getExtendedName ()+' '+'IN '+' '+' BinaryRelation '+' ( '+ u
.
eContainingClass . name+' , '+u . eReferenceType . name+' ) '
else i f
202
(u . lowerBound=0 and u . upperBound=-1)and(u . eOpposite .
lowerBound=0 and u .
eOpposite . upperBound=1) then
u . getExtendedName ( )+' '+'IN '+' '+' PartialFunction '+' ( '+
u .
eContainingClass . name+' , '+u . eReferenceType . name+' ) '
204
else i f
(u . lowerBound=0 and u . upperBound=-1)and(u . eOpposite .
lowerBound=1 and u .
eOpposite . upperBound=1) then
206
u . getExtendedName ( )+' '+'IN '+' '+' TotalFunction '+' ( '+ u
.
eContainingClass . name+' , '+u . eReferenceType . name+' ) '
else i f
208
(u . lowerBound=0 and u . upperBound=1)and(u . eOpposite .
lowerBound=0 and u .
eOpposite . upperBound=1) then
u . getExtendedName ( )+' '+'IN '+' '+' PartialInjective '+' ( '+
u .
eContainingClass . name+' , '+u . eReferenceType . name+' ) '
210
else i f
(u . lowerBound=0 and u . upperBound=1)and(u . eOpposite .
lowerBound=1 and u .
eOpposite . upperBound=1) then
212
u . getExtendedName ( )+' '+'IN '+' '+' TotalInjective '+' ( '+ u
.
eContainingClass . name+' , '+u . eReferenceType . name+' ) '
else i f
214
(u . lowerBound=1 and u . upperBound=-1)and(u . eOpposite .
lowerBound=0 and u .
eOpposite . upperBound=1) then
u . getExtendedName ( )+' '+'IN '+' '+' PartialSurjective '+' (
'+ u .
eContainingClass . name+' , '+u . eReferenceType . name+' ) '
216
page 107
else i f
218
(u . lowerBound=1 and u . upperBound=-1)and(u . eOpposite .
lowerBound=1 and u .
eOpposite . upperBound=1) then
u . getExtendedName ( )+' '+'IN '+' '+' TotalSurjective '+' ( '+
u .
eContainingClass . name+' , '+u . eReferenceType . name+' ) '
220
else i f
(u . lowerBound=1 and u . upperBound=1)and (u . eOpposite .
lowerBound=1 and u .
eOpposite . upperBound=1) then
222
u . getExtendedName ( )+' '+'IN '+' '+' TotalBijective '+' ( '+ u
.
eContainingClass . name+' , '+u . eReferenceType . name+' ) '
else i f
224
(u . lowerBound=1 and u . upperBound=1)and(u . eOpposite .
lowerBound=0 and u .
eOpposite . upperBound=1) then
226
u . getExtendedName ( )+' '+'IN '+' '+' PartialBijective '+' ( '+
u . eContainingClass . name+' , '+u . eReferenceType . name+' ) '
else
228
230
u . getExtendedName ( )+' '+'IN '+' '+' TotalBijective '+' ( '+ u
. eContainingClass . name+' , '+u . eReferenceType . name+' ) '
232
234
236
endif endif endif endif endif endif endif endif
238
240
endif
242
) ,
244
sss :MM1! Event (
name <- 'INITIALISATION' , actions <-Sequence{actionA} )
,
246
248
actionA : MM1! Action (
name <-' act ',
predicat <-u . getExtendedName ( )+' := '+' isEmpty () '
)
250
}
252
254
page 108
rule Eoperation2Event {
256
from
H: MM! EOperation
258
to
evt : MM1! Event (
260
name <- H. name ,
parameters <-H. eParameters ,
guards <- Sequence {thisModule . GetEParameter->c o l l e c
t ( e | thisModule .
resolveTemp (e , ' grd ' ) )}
|
|
|
|
|
|
|
|
)
|
|
|
|
262
|
|
|
|
|
|
|
|
}
|
|
|
|
264
|
|
rule EParameter2ParameterAndGuard { from
|
|
|
266
|
|
|
|
Z: MM! EParameter
|
|
|
|
|
|
to
|
|
|
268 270 272 274 276
|
|
|
|
ZZ: MM1! Parameter ( name <- Z. name
) ,
grd : MM1! Guard (
name <- ' gdr1 ',
predicat <-Z. name+' '+'IN '+' '+Z. eType . name
)
|
|
|
278 }
|
|
|
|
|
|
ECore2Event-B.atl
|
|
page 109
110
D Le template de génération de code
6
8
10
12
14
16
18
20
22
24
26
28
2 IMPORT EventB
DEFINE main FOR ROOT
4 EXPAND Contenu_Context FOREACH contextes
EXPAND Contenu_machine FOREACH machines
ENDDEFINE
REM ******* ICI ON PRESENTE LE CONTENU DU
contexte ******ENDREM
DEFINE Contenu_Context FOR C ont ext
FILE name+" .buc"
Context
name
EXPAND EXTENDS FOREACH ex t ends
I F sets . isEmpty
SETS
EXPAND SETS FOREACH s e t s
ENDIF
I F constants. isEmpty
CONSTANTS
EXPAND CONSTANTS FOREACH cons t a n t s
ENDIF
I F axioms. isEmpty
AXIOMS
EXPAND AXIOMS FOREACH axioms
ENDIF
I F theorems. isEmpty
THEOREMS
EXPAND THEOREMS FOREACH theorems
ENDIF
EventB en Xpand
END
ENDFILE
ENDDEFINE
DEFINE EXTENDS FOR Context
I F ! extends. isEmpty
EXTENDS
this . extends . toString ()
ENDIF
ENDDEFINE
DEFINE SETS FOR Sets
this . name
ENDDEFINE
DEFINE CONSTANTS FOR Constants
this . name
ENDDEFINE
DEFINE AXIOMS FOR Axioms
t h i s . name : t h i s . p r e d i c a t
30 32 34 36 38 40 42 44 46 48 50
ENDDEFINE
DEFINE THEOREMS FOR Theorems t h i s . name : t h i s . p r e d i
c a t ENDDEFINE
REM ******* ICI ON PRESENTE LE CONTENU DU
MACHINE******ENDREM 52 DEFINE Contenu_machine
FOR Machine
FILE name+" .bum"
54 56 58 60 62 64 66
MACHINE
page 111
name
I F ! refines . isEmpty
REFINES
FOREACH r e fin e s . name AS e ITERATOR i t e r SEPARATOR''
e
ENDFOREACH
ENDIF
I F ! Sees . isEmpty
SEES
FOREACH Sees . name AS e ITERATOR i t e r SEPARATOR'' e
ENDFOREACH
ENDIF
I F ! variables. isEmpty
VARIABLES
EXPAND VARIABLES FOREACH variables
ENDIF
I F ! invariants . isEmpty
INVARIANTS
EXPAND INVARIANTS FOREACH invariants
ENDIF
I F ! variants . isEmpty
VARIANT
EXPAND INVARIANTS FOREACH invariants
ENDIF
I F ! events. isEmpty
EVENTS
EXPAND EVENTS FOREACH events
ENDIF
END
ENDFILE
ENDDEFINE
DEFINE VARIABLES FOR Variable
I F name. trim () . length !=0
this . name
ENDIF
ENDDEFINE
DEFINE INVARIANTS FOR Invariant
I F name. trim () . length !=0 && predicat . trim () .
length !=0
this . name : this. p r e d i c a t
ENDIF
ENDDEFINE
DEFINE EVENTS FOR Event
n a m e
I F extended
extended
ENDIF
STATUS
68 70 72 74 76 78 80 82 84 86 88 90 92 94 96 98 100 102
104
106
REFINES
I F ! refines . isEmpty
page 112
EXPAND REFINES FOREACH r e f i n e s
108
110
112
114
116
118
120
122 124 126 128
130
132
134
136
138
140
ENDIF
I F ! parameters . isEmpty && guards . isEmpty &&
Witnesses . isEmpty && actions . isEmpty
ANY
EXPAND PARAMETER FOREACH parameters
BEGIN
ELSEIF ! parameters . isEmpty && ! guards . isEmpty
&& Witnesses.
isEmpty && actions . isEmpty
ANY
EXPAND PARAMETER FOREACH parameters
WHERE
EXPAND GUARDS FOREACH guards
THEN
skip
ELSEIF ! parameters . isEmpty && ! Witnesses . isEmpty
&& guards.
isEmpty && actions . isEmpty
ANY
EXPAND PARAMETER FOREACH parameters WITH
EXPAND WITNESSES FOREACH Witnesses BEGINREM Then <ENDREM
skip
ELSEIF ! parameters . isEmpty && ! actions . isEmpty
&& guards. isEmpty && witnesses . isEmpty
ANY
EXPAND PARAMETER FOREACH
paramet ers
BEGINREMThenENDREM
EXPAND ACTION FOREACH actions
ELSEIF ! parameters . isEmpty && ! actions . isEmpty
&& ! guards. isEmpty && ! Witnesses . isEmpty &&
actions. i s E m p t y
ANY
EXPAND PARAMETER FOREACH
paramet ers
WHERE
page 113
EXPAND GUARDS FOREACH guards
142
144
146
148 150 152 154 156
158
160
162
164
166
168
170
172
174
WITH EXPAND WITNESSES FOREACH Witnesses THEN skip
ELSEIF parameters . isEmpty && actions . isEmpty
&& guards. isEmpty && Witnesses . isEmpty && actions .
isEmpty
ANY
EXPAND PARAMETER FOREACH parameters
WHERE
EXPAND GUARDS FOREACH guards
WITH
EXPAND WITNESSES FOREACH Witnesses
THEN
EXPAND ACTION FOREACH actions
ELSEIF actions . isEmpty && parameters . isEmpty
&& guards.
isEmpty && Witnesses. isEmpty
ANY
EXPAND PARAMETER FOREACH parameters
WHERE
EXPAND GUARDS FOREACH guards
THEN
EXPAND ACTION FOREACH actions
ELSEIF guards . isEmpty && Witnesses . isEmpty &&
parameters.
isEmpty && actions . isEmpty
WHERE EXPAND GUARDS FOREACH guards THEN skip
skip
ELSEIF guards . isEmpty && Witnesses . isEmpty &&
parameters.
isEmpty && actions . isEmpty
WHERE
EXPAND GUARDS FOREACH guards
WITH
EXPAND WITNESSES FOREACH Witnesses
THEN
page 114
ELSEIF guards . isEmpty && actions . isEmpty &&
Witnesses . isEmpty && parameters . isEmpty
176
178
WHERE
EXPAND GUARDS FOREACH guards
THEN
180
EXPAND ACTION FOREACH actions
ELSEIF guards . isEmpty && Witnesses . isEmpty &&
actions.
isEmpty && parameters. isEmpty
182
WHERE
EXPAND GUARDS FOREACH guards
184
WITH
EXPAND WITNESSES FOREACH Witnesses
186
THEN
EXPAND ACTION FOREACH actions
188
ELSEIF Witnesses . isEmpty && parameters . isEmpty
&& guards.
isEmpty && actions . isEmpty
WITH
190
EXPAND WITNESSES FOREACH Witnesses
BEGINREMThenENDREM
192
skip
ELSEIF Witnesses . isEmpty && actions . isEmpty
&& parameters.
isEmpty && guards. isEmpty
194
196
WITH EXPAND WITNESSES FOREACH Witnesses BEGIN EXPAND ACTION
FOREACH actions
198
i . name
208
ELSEIF actions . isEmpty && parameters . isEmpty
&& guards.
isEmpty && Witnesses. isEmpty
BEGIN
200
EXPAND ACTION FOREACH actions
ELSE
202
skip
ENDIF
204
END
ENDDEFINE
206
DEFINE REFINES FOR Event
FOREACH refines AS i SEPARATOR ' '
page 115
210
212
214
216
218
220
222
ENDFOREACH
ENDDEFINE
DEFINE PARAMETER FOR Parameter
this . name
ENDDEFINE
DEFINE GUARDS FOR Guard
this . name : this. p r e d i c a t
ENDDEFINE
DEFINE WITNESSES FOR Witness
this . name : this. p r e d i c a t
ENDDEFINE
DEFINE ACTION FOR Action
this . name : this . p r e d i c a t
ENDDEFINE
page 116
| 
