User friendly version of the CCSL grammar

• | denotes alternative
  
• [] denotes an optional occurence
  
• {} denotes repetition (including zero)
  
• UPPER-CASE symbols are terminals, they denote either keywords or symbolic tokens

file:
    { declaration } EOF


declaration:
    classspec
  | adtspec
  | groundsignature
  | typedef
  | groundtermdef


classspec:
    BEGIN identifier [ parameterlist ] COLON [ FINAL ] CLASSSPEC { importing } { classsection } END identifier


parameterlist:
    OBRACKET parameters { COMMA parameters } CBRACKET


parameters:
    identifier { COMMA identifier } COLON [ variance ] TYPE


variance:
    POS
  | NEG
  | MIXED
  | OPAREN numberorquestion COMMA numberorquestion CPAREN


numberorquestion:
    QUESTIONMARK
  | VALUE


classsection:
    inheritsection
  | [ visibility ] attributesection [ SEMICOLON ]
  | [ visibility ] methodsection [ SEMICOLON ]
  | definitionsection
  | classconstructorsection [ SEMICOLON ]
  | assertionsection
  | creationsection
  | theoremsection
  | requestsection [ SEMICOLON ]


visibility:
    PUBLIC
  | PRIVATE


inheritsection:
    INHERIT FROM ancestor { COMMA ancestor }


ancestor:
    identifier [ argumentlist ] [ RENAMING renaming { AND renaming } ]


renaming:
    identifier AS identifier


attributesection:
    ATTRIBUTE member { SEMICOLON member }


methodsection:
    METHOD member { SEMICOLON member }


definitionsection:
    DEFINING member formula SEMICOLON { member formula SEMICOLON }


classconstructorsection:
    CONSTRUCTOR member { SEMICOLON member }


member:
    identifier COLON type


assertionsection:
    ASSERTION { importing } [ assertionselfvar ] { freevarlist } namedformula { namedformula }


assertionselfvar:
    SELFVAR identifier COLON SELF


freevarlist:
    VAR vardeclaration { SEMICOLON vardeclaration }


creationsection:
    CREATION { importing } { freevarlist } namedformula { namedformula }


theoremsection:
    THEOREM { importing } { freevarlist } namedformula { namedformula }


namedformula:
    identifier COLON formula SEMICOLON


requestsection:
    REQUEST request { SEMICOLON request }


request:
    identifier COLON type


formula:
    FORALL OPAREN vardeclaration { COMMA vardeclaration } CPAREN colonordot formula
  | EXISTS OPAREN vardeclaration { COMMA vardeclaration } CPAREN colonordot formula
  | LAMBDA OPAREN vardeclaration { COMMA vardeclaration } CPAREN colonordot formula
  | LET binding { semicolonorcomma binding } [ semicolonorcomma ] IN formula
  | formula IFF formula
  | formula IMPLIES formula
  | formula OR formula
  | formula AND formula
  | IF formula THEN formula { elseif formula THEN formula } ELSE formula
  | NOT formula
  | formula infix_operator formula
  | ALWAYS formula FOR [ identifier [ argumentlist ] DOUBLECOLON ] methodlist
  | EVENTUALLY formula FOR [ identifier [ argumentlist ] DOUBLECOLON ] methodlist
  | CASES formula OF caselist [ semicolonorcomma ] ENDCASES
  | formula WITH OBRACKET update { COMMA update } CBRACKET
  | formula DOT qualifiedid
  | formula formula
  | TRUE
  | FALSE
  | PROJ_N
  | VALUE
  | qualifiedid
  | OPAREN formula COLON type CPAREN
  | OPAREN formula { COMMA formula } CPAREN


colonordot:
    COLON
  | DOT


vardeclaration:
    identifier { COMMA identifier } COLON type


methodlist:
    OBRACE identifier { COMMA identifier } CBRACE


qualifiedid:
    idorinfix
  | identifier [ argumentlist ] DOUBLECOLON idorinfix


idorinfix:
    OPAREN infix_operator CPAREN
  | identifier


binding:
    identifier [ COLON type ] EQUAL formula


elseif:
    ELSEIF
  | ELSIF


semicolonorcomma:
    COMMA
  | SEMICOLON


caselist:
    pattern COLON formula { semicolonorcomma pattern COLON formula }


pattern:
    identifier [ OPAREN identifier { COMMA identifier } CPAREN ]


update:
    formula ASSIGN formula


adtspec:
    BEGIN identifier [ parameterlist ] COLON ADT { adtsection } END identifier


adtsection:
    adtconstructorlist [ SEMICOLON ]


adtconstructorlist:
    CONSTRUCTOR adtconstructor { SEMICOLON adtconstructor }


adtconstructor:
    identifier [ adtaccessors ] COLON type


adtaccessors:
    OPAREN identifier { COMMA identifier } CPAREN


groundsignature:
    BEGIN identifier [ parameterlist ] COLON GROUNDSIGNATURE { importing } { signaturesection } END identifier


signaturesection:
    typedef
  | signaturesymbolsection [ SEMICOLON ]


typedef:
    TYPE identifier [ parameterlist ] [ EQUAL type ]


signaturesymbolsection:
    CONSTANT termdef { SEMICOLON termdef }


groundtermdef:
    CONSTANT termdef [ SEMICOLON ]


termdef:
    idorinfix [ parameterlist ] COLON type [ formula ]


type:
    SELF
  | CARRIER
  | BOOL
  | OBRACKET type { COMMA type } ARROW type CBRACKET
  | OBRACKET type { COMMA type } CBRACKET
  | type STAR type { STAR type }
  | type ARROW type
  | OPAREN type CPAREN
  | qualifiedid
  | identifier argumentlist


argumentlist:
    OBRACKET type { COMMA type } CBRACKET


importing:
    IMPORTING identifier [ argumentlist ]

Reserved words

adt always and as assertion attribute begin bool carrier cases classspec constant constructor creation defining else elseif elsif end endcases eventually exists false final for forall from groundsignature groundterm groundtype if iff implies importing in inherit lambda let method mixed neg not of or pos private public renaming request self selfvar then theorem true type var with

Identifiers

Infix operators

!    $    &    *    +    -    .    /    \    :    <    =    >    ?    @    ^    |    ~    #

$    &    *    +    -    /    \    <    =    >    @    ^    |    ~    #

• operators starting with **   : right associative
• starting with *,  / , or  \  : left associative
• starting with + or -   : left associative
• starting with one of @, ^ or #   : left associative
• starting with either =, ~, <, >, |, & or $   : non-associative

• =    for equality
• ~    for behavioral equality

Symbols

ARROW	->		EOF	<end of input>
ASSIGN	:=		EQUAL	=
CBRACE	}		OBRACE	{
CBRACKET	]		OBRACKET	[
COLON	:		OPAREN	(
COMMA	,		QUESTIONMARK	?
CPAREN	)		SEMICOLON	;
DOT	.		VALUE	<a sequence of digits>
DOUBLECOLON	::