Syntaxe EBNF d'un sous-ensemble du langage Spec

module :
     definition
   | function
   | machine
   | type
   ;

definition :
   "DEFINITION" entete_module concepts "END"
   ;

function :
   "FUNCTION" entete_module messages concepts "END"
   ;

machine :
   "MACHINE" entete_module state messages concepts "END"
   ;

type :
   "TYPE" entete_module model messages concepts "END"
   ;

entete_module :
   IDENTIFICATEUR { "{" formels "}" }
   ( "INHERIT" nom_effectif )*
   ( "IMPORT" (IDENTIFICATEUR)+ "FROM" nom_effectif )*
   ;

messages :
   ( message )+
   ( message_temporel )*
   ;

message :
   "MESSAGE" { "EXCEPTION" } { IDENTIFICATEUR } { "(" formels ")" }
   reponse
   ;

message_temporel :
  "TEMPORAL" IDENTIFICATEUR contrainte_temporelle reponse
   ;

reponse :
     reponse_incond
   | reponses_conds
   ;

reponse_incond :
   { "CHOOSE" "(" formels ")" }
   { "REPLY" message_effectif where }
   ( "SEND" message_effectif "TO" nom_effectif where {foreach} )*
   { "TRANSITION" liste_expressions }
   ;

reponses_conds :
   ( "WHEN" liste_expressions reponse_incond )+ 
   "OTHERWISE" reponse_incond
   ;

message_effectif :
   { "EXCEPTION" } { nom_effectif } { "(" formels ")" }
   ;

where :
   { "WHERE" liste_expressions }
   ;

contrainte_temporelle :
  "WHERE" liste_expressions
   ;

foreach :
   "FOREACH" "(" formels ")"
   ;

model :
   { "MODEL" { "(" formels ")" } invariant }
   ;

state :
   { "STATE" { "(" formels ")" } invariant initially }
   ;

invariant :
   "INVARIANT" liste_expressions
   ;

initially :
   "INITIALLY" liste_expressions
   ;

concepts :
   ( concept )*
   ;

concept :
     "CONCEPT" IDENTIFICATEUR ":" nom_type where
   | "CONCEPT" IDENTIFICATEUR "(" formels ")" "VALUE" "(" formels ")" where
   ;

formels :
   declaration ( "," declaration )* restriction
   ;

declaration :
   ( IDENTIFICATEUR )+ ":" nom_type
   ;

restriction :
   { "SUCH THAT" liste_expressions }
   ;

nom_effectif :
   IDENTIFICATEUR { "@" nom_effectif } { "{" liste_expressions "}" }
   ;

liste_expressions :
   expression ( "," expression )*
   ;

expression :
     expression_unaire
   | expression_binaire
   | expression_appel
   | expression_temporelle
   | quantificateur "(" formels "::" expression ")"
   | nom_effectif
   | constante
   | "?"
   | "!"
   | DELAY
   | PERIOD
   | TIME
   | "(" expression ")"
   ;

expression_unaire :
   operateur_unaire expression
   ;

expression_binaire :
   expression operateur_binaire expression
   ;

operateur_unaire :
   "~" | "+" | "-" | "*" | "$"
   ;

operateur_binaire :
   "<=>" | "=>" | "|" | "&" |
   "<" | ">" | "=" | "<=" | ">=" | "==" |
   "~=" | "~<" | "~>" | "~<=" | "~>=" | "~==" |
   "IN" | "U" | 
   "@" | "||" | 
   "+" | "-" | "*" | "/" | "^" |
   "MOD" | "MIN" | "MAX"
   ;

expression_appel :
   expression
   ( "[" liste_expressions "]" 
      | 
     "(" liste_expressions ")" 
      | 
     "." IDENTIFICATEUR 
   )*
   ;
   
expression_temporelle :
  "(" expression constante_duration ")"
   ;

quantificateur :
     "ALL"
   | "SOME"
   | "SUM"
   | "PRODUCT"
   | "NUMBER"
   | "MAXIMUM"
   | "MINIMUM"
   | "UNION"
   | "INTERSECTION"
   ;

constante :
     CONSTANTE_ENTIER
   | CONSTANTE_REEL
   | CONSTANTE_CARACTERE
   | CONSTANTE_CHAINE
   | "#" IDENTIFICATEUR
   | ensemble
   | sequence
   | dictionnaire
   | tuple
   ;

constante_duration :
   /* voir le type duration de la librairie Spec */
   ;

ensemble :
   ensemble_extension | ensemble_intervalle | ensemble_comprehension
   ;

sequence :
   sequence_extension | sequence_intervalle | sequence_comprehension
   ;

dictionnaire :
   "{" { paire ("," paire)* } ";" expression "}"
    ;

paire :
   "[" expression "," expression "]"
   ;

tuple :
   "["      IDENTIFICATEUR "::" expression 
       ("," IDENTIFICATEUR "::" expression)* 
   "]"
   ;

ensemble_extension :
   "{" { liste_expressions } "}"
   ;

sequence_extension :
   "[" { liste_expressions } "]"
   ;

ensemble_intervalle :
   "{" expression ".." expression "}"
   ;

sequence_intervalle :
   "[" expression ".." expression "]"
   ;

sequence_comprehension :
   "[" declaration ( "," declaration )* restriction "::" expression "]"
   ;

ensemble_comprehension :
   "{" declaration ( "," declaration )* restriction "::" expression "}"
    ;

nom_type :
     "type"
   | "nat"
   | "integer"
   | "real"
   | "char"
   | "string"
   | "set" "{" nom_type "}"
   | "sequence" "{" nom_type "}"
   | "map" "{" nom_type "," nom_type "}"
   | "tuple" "{" IDENTIFICATEUR "::" nom_type ( "," IDENTIFICATEUR "::" nom_type )* "}"
   | "enumeration" "{" IDENTIFICATEUR ("," IDENTIFICATEUR)* "}"
   | IDENTIFICATEUR { "{" expression ("," expression)* "}" }
   ;