// ----------------------------------------------------------------------  
// specifications  
// ----------------------------------------------------------------------  
 
// a unit specification  
unitspec:  
  imports ’theory’ ( ’uses’ names )? ’{’ declarations ’}’ EOF ;  
 
// a class specification  
classspec: ( ’invariant’ formula ’;’ )? EOF ;  
 
// a method specification  
methodspec:  
  ( ’helper’ ’;’ )?  
  ( ’requires’ formula ’;’ )?  
  ( ’assignable’ names ’;’ )?  
  ( ’signals’ names ’;’ )?  
  ( ’ensures’ formula ’;’ )?  
  ( ’diverges’ formula ’;’ )?  
  ( ’decreases’ term ( ’,’ term )* ’;’ )?  
  EOF ;  
 
// a loop annotation  
loopspec:  
  ( ’invariant’ formula ’;’ )?  
  ( ’decreases’ term ( ’,’ term )* ’;’ )?  
  EOF ;  
 
// a command pre-state annotation  
statementspec: ( ’assert’ formula ’;’ )? ;  
 
// a theory declaration  
theorydecl:  
  ( ’package’ name ’;’ )? imports  
  ( ’public’ )* ’theory’ IDENT ( ’uses’ names )?  
  ’{’ ( ( declaration )? ’;’ )* ’}’ EOF ;  
 
imports: ( ’import’ name ( ’.’ ’*’ )? ’;’ )* ;  
 
declarations: ( ( declaration )? ’;’ )* ;  
 
declaration:  
  IDENT ’:’  
  ( ’TYPE’  
  | ’TYPE’ ’=’ typeExp  
  | ’FORMULA’ formula  
  | ’AXIOM’ formula  
  | typeExp ( ’=’ term |  
              ’=’ ’PRED’ paramList ’:’ formula |  
              ’<=>’ formula )?  
  ) ;  
 
typeExp:  
( typeExpBase ’->’ typeExp  
| ’(’ typeExp ( ’,’  typeExp )+  ’)’ ’->’ typeExp  
| ’ARRAY’ typeExpBase ’OF’ typeExp  
| typeExpBase  
) ;  
 
typeExpBase:  
( name  
| ’BOOLEAN’  
| ’LOGICAL’  
| ’BIT’  
| ’INT’  
| ’NAT’  
| ’REAL’  
| ’STRING’  
| ’STATE’ ( ’(’ typeExp ’)’ )?  
| ’[’ typeExp ( ’,’  typeExp )+  ’]’  
| ’[’ typeExp ’]’  
| ’[#’ IDENT ’:’ typeExp ( ’,’ IDENT ’:’ typeExp )* ’#]’  
| ’SUBTYPE’ ’(’ term ’)’  
| ’[’ term ’..’ term ’]’  
| ’PREDICATE’ ( ’(’ typeExp ( ’,’  typeExp )*  ’)’ )?  
| ’(’ typeExp ’)’ ) ;  
 
// ----------------------------------------------------------------------  
// formulas  
// ----------------------------------------------------------------------  
 
// quantifiers bind weakest  
formula:  
( ’FORALL’ paramList ’:’ formula  
| ’EXISTS’ paramList ’:’ formula  
| formula10  
) ;  
 
// lets  
formula10:  
( ’LET’ vdefinition ( ’,’ vdefinition )* ’IN’ formula10  
| formula20  
) ;  
 
// implications, equivalences, exclusive ors (= non-equivalences)  
formula20:  
( formula30 ’=>’ formula20  
| formula30 ( ’<=>’ formula30 | ’XOR’ formula30 )?  
) ;  
 
// disjunctions  
formula30: formula40 ( ’OR’ formula40 )* ;  
 
// conjunctions  
formula40: formula50 ( ’AND’ formula50 )* ;  
 
// logical negations  
formula50: ’NOT’ formula50 | formula60 ;  
 
// equality and inequality and relations  
formula60:  
  term  
  ( ’=’ term | ’/=’ term | ’<’ term | ’<=’ term | ’>’ term | ’>=’ term )  
| formula70 ;  
 
// atomic predicates  
formula70:  
  name ’(’ term ( ’,’ term )* ’)’  
| ’EXECUTES’ ’@’ statearg | ’CONTINUES’ ’@’ statearg  
| ’BREAKS’ ’@’ statearg | ’RETURNS’ ’@’ statearg  
| ’THROWS’ ’@’ statearg | ’THROWS’ ’(’ name ’)’ ’@’ statearg  
| formula100 ;  
 
// argument to state predicate  
statearg: ’NOW’ | ’NEXT’ | name ;  
 
// atoms  
formula100:  
  ( name | ’(’ ’OLD’ name ’)’ | ’(’ ’VAR’ name ’)’ )  
  ( ’.’ ( NUMBER | IDENT ) | ’[’ term ’]’ )*  
| ’TRUE’ | ’FALSE’  
| ’IF’ formula ’THEN’ formula  
   ( ’ELSIF’ formula ’THEN’ formula )* ’ELSE’ formula ’ENDIF’  
| ’WRITESONLY’ names | ’READSONLY’  
| ’(’ formula ’)’  
;  
 
// ----------------------------------------------------------------------  
// terms  
// ----------------------------------------------------------------------  
 
// quantifiers bind weakest  
term: ’LAMBDA’ paramList ’:’ term | ’ARRAY’ paramList ’:’ term | term10 ;  
 
// lets  
term10: ’LET’ vdefinition ( ’,’ vdefinition )* ’IN’ term10 | term20 ;  
 
// sums and differences  
term20: term30 ( ’+’ term30 | ’-’ term30 | ’|’ term30 )* ;  
 
// products and quotients  
term30: term40 ( ’*’ term40 | ’/’ term40 | ’&’ term40 )* ;  
 
// power terms  
term40: term50 ( ’^’ term50 )* ;  
 
// unary arithmetic operators  
term50: ’+’ term50 | ’-’ term50 | ’~’ term50 | term60 ;  
 
// updates  
term60:  
  term70  
  ( ’WITH’ ( ’.’ ( NUMBER | IDENT ) | ’[’ term ’]’ )+ ’:=’ term70 )* ;  
 
// selections  
term70: term80 ( ’.’ ( NUMBER | IDENT ) | ’[’ term ’]’ )* ;  
 
// applications  
term80:  
  ’VALUE’ ’@’ term100 | ’MESSAGE’ ’@’ term100  
| term100 ( ’(’ term ( ’,’ term )* ’)’ )* ;  
 
// atoms  
term100:  
  name | NUMBER | STRING | ’TRUE’ | ’FALSE’  
| ’LOGICALTRUE’ | ’LOGICALFALSE’ | ’BITTRUE’ | ’BITFALSE’  
| ’OLD’ name | ’VAR’ name | ’NOW’ | ’NEXT’  
| ’(’ term ( ’,’  term )* ’)’  
| ’(#’ IDENT ’:=’ term ( ’,’ IDENT ’:=’ term )* ’#)’  
| ’IF’ formula ’THEN’ term  
  ( ’ELSIF’ formula ’THEN’ term )* ’ELSE’ term ’ENDIF’ ;  
 
// ----------------------------------------------------------------------  
// auxiliaries  
// ----------------------------------------------------------------------  
 
paramList: ’(’ param[params] ( ’,’ param[params] )* ’)’ ;  
 
param: IDENT ( ’,’ IDENT )* ’:’ typeExp ;  
 
// value definition  
vdefinition: IDENT ’:’ typeExp  ’=’ term | IDENT ’=’ term ;  
 
// a name  
name: IDENT ( ’.’ IDENT )* ;  
 
// a sequence of names  
names: name ( ’,’ name )* ;  
 
// ----------------------------------------------------------------------  
// lexical syntax  
// ----------------------------------------------------------------------  
 
IDENT: REALLETTER (LETTER | DIGIT)* ;  
NUMBER: DIGIT (DIGIT)* ;  
STRING : ’~’ (~(’~’ | ’\\’ | EOL) | ESCAPED )* ’~’ ;  
REALLETTER: (’a’..’z’ | ’A’..’Z’ );  
LETTER: ( REALLETTER | ’_’);  
DIGIT: (’0’..’9’);  
WS: (’ ’ | ’\t’ | EOL | COMMENT) { $channel=HIDDEN; };  
EOL: (’\n’ | ’\r’ | ’\f’);  
COMMENT : ’//’ .* EOL | ’/*’ .* ’*/’ ;  
ESCAPED : ’\\’  
  ( ’\\’ | ’~’ | ’\’’ | ’n’ | ’t’ | ’b’ | ’f’ | ’r’ |  
    (’u’ HEX HEX HEX HEX) ) ;  
HEX : ’0’..’9’ | ’a’..’f’ | ’A’..’F’ ;