A Grammar Summary

The following is a summary of the context-free grammar for Larch/C++. See section 3 Syntax Notation for the notation used. In the first section below, grammatical productions are to be understood lexically. That is, no white space (see section 4.1 White Space) may intervene between the characters of a token.

11.13 Lexical Conventions

microsyntax ::= lexeme [ lexeme ] ...
lexeme ::= white-space | comment | annotation-marker
          | pragma | token
white-space ::= non-nl-white-space | newline
non-nl-white-space ::= a blank, tab, vertical tab, carriage return, or formfeed character
newline ::= a newline character
comment ::= C-style-comment | C++-style-comment
C-style-comment ::= /* [ C-style-body ] C-style-end
C-style-body ::= non-at-star [ non-star-slash ] ...
        | stars-non-slash [non-star-slash] ...
non-star-slash ::= non-star
        | stars-non-slash
stars-non-slash ::= * [ * ] ... non-slash
non-at-star ::= any character except @ or *
non-star ::= any character except *
non-slash ::= any character except /
C-style-end ::= [ * ] ... */
C++-style-comment ::= // newline
       | // non-at-newline [ non-newline ] ... newline
non-newline ::= any character except a newline
non-at-newline ::= any character except @ or newline
annotation-marker ::= //@ | /*@ | @*/
pragma ::= # non-nl-white-space pragma [ non-newline ] ...
         | __attribute__ [ non-semi-newline ] ...
         | __asm__ | __const__ | __inline__
         | __signed__ | __typeof__ | __volatile__
         | __extension__
non-semi-newline ::= any character except a semicolon (;) or newline
token ::= identifier | simple-id
        | keyword | context-dependent-keyword
        | special-symbol | predicate-keyword
        | informal-comment | literal | lsl-constant
identifier ::= letter [ letter-or-digit ] ...
            | ident( letter [ letter-or-digit ] ... )
letter ::= _, a through z, or A through Z
digit ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9
letter-or-digit ::= letter | digit
identifier ::= letter [ letter-or-digit ] ...
keyword ::= term-only-keyword | stmt-exp-only-keyword
    | always-keyword
term-only-keyword ::= fresh | informally | liberally
    | on          | nothing     | post
    | pre         | redundantly | result
    | returns     | self        | then
    | thrown      | throws      | trashed
    | unchanged   
stmt-exp-only-keyword ::= break | case | catch
    | const_cast  | continue    | default
    | delete      | dynamic_cast| goto       
    | new         | reinterpret_cast| return     
    | static_cast | switch      | throw      
    | try         | typeid
always-keyword ::= abstract | accesses | also
   | any         | asm         | assert      
   | assume      | auto        | behavior    
   | be          | by          | calls       
   | char        | choose      | class       
   | constraint  | constructs  | const       
   | decreasing  | depends     | double      
   | do          | else        | ensures     
   | enum        | everything  | example     
   | expects     | explicit    | extern      
   | float       | for         | friend      
   | if          | inline      | int         
   | invariant   | is          | let         
   | long        | maintaining | modifies    
   | mutable     | namespace   | operator    
   | or          | private     | program     
   | protected   | public      | reach       
   | refine      | register    | represents  
   | requires    | satisfies   | short       
   | signature   | signed      | simulates   
   | sizeof      | spec        | static      
   | struct      | template    | this        
   | throw       | trashes     | typedef     
   | typename    | union       | unsigned    
   | uses        | using       | virtual     
   | void        | volatile    | wchar_t     
   | weakly      | where       | while       
   | with        
context-dependent-keyword ::= typedef-non-class-or-enum-name
    | typedef-class-name | typedef-enum-name
    | original-namespace-name | namespace-alias-name
    | original-class-name | original-enum-name
    | template-non-class-name | template-class-name
typedef-non-class-or-enum-name ::= identifier
typedef-class-name ::= identifier
typedef-enum-name ::= identifier
original-namespace-name ::= identifier
namespace-alias-name ::= identifier
original-class-name ::= identifier
original-enum-name ::= identifier
template-non-class-name ::= identifier
template-class-name ::= identifier
special-symbol ::= always-special-symbol
    | C++-decl-symbol | C++-operator-symbol
    | predicate-special-symbol | lsl-op
always-special-symbol ::= ( | ) | { | } | [ | ]
        | = | ; | : | :: | ,
        | ? | . | .* | `...'
C++decl-symbol ::= < | > | * | & | ~
C++-operator-symbol ::= new | delete
 | new [ non-nl-white-space ] ... [] | delete [ non-nl-white-space ] ...  []
 | +   | -   | *   | /   | %   | ^   | &   | `|' | ~
 | !   | =   | <   | >   | +=  | -=  | *=  | /=  | %=
 | ^=  | &=  | |=  | <<   | >>  | >>= | <<= | ==  | !=
 | <=  | >=  | &&  | `||' | ++  | --  | ,   | ->* | ->
 | ()  | []
predicate-symbol ::= ^ | ' | \< | \>
lsl-op ::= \ identifier | star-or-op-char [ op-char ] ...
star-or-op-char ::= * | op-char
op-char ::= ~ | = | < | > | + | - | /
          | ! | # | $ | & | ? | @ | `|'
predicate-keyword ::= \A | \and | \any | \E | \eq | \exists | \forall
     | \implies | \langle | \neq | \obj | \or | \pre | \post | \rangle
     | = | == | != | ~= | /\ | \/ | =>
informal-comment ::= (% [ informal-comment-body ] %)
informal-comment-body ::= non-percent-right-paren [ non-percent-right-paren ] ...
non-percent-right-paren ::= non-percent
          | percents-non-right-paren 
non-percent ::= any character except %
percents-non-right-paren ::= % [ % ] ... non-right-paren
non-right-paren ::= any character except )
literal ::= integer-constant | floating-constant
      | character-constant | string-literal [ string-literal ] ...
      | abstract-string-literal
integer-constant  ::= decimal-constant | octal-constant | hex-constant
decimal-constant ::= one-to-nine [ digit ] ... [integer-suffix]
one-to-nine      ::= 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9
octal-constant   ::= 0 [ octal-digit ] ... [integer-suffix]
octal-digit      ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7
hex-constant     ::= 0 hex-indicator hex-digit [ hex-digit ] ... [integer-suffix]
hex-indicator    ::= x | X
hex-digit        ::= digit | a | b | c | d | e | f | A | B | C | D | E | F
integer-suffix   ::= long-suffix | unsigned-suffix
        | long-suffix unsigned-suffix | unsigned-suffix long-suffix
long-suffix ::= l | L
unsigned-suffix ::= u | U
floating-constant   ::= fractional-constant [exponent-part] [float-suffix]
                   | digit [ digit ] ... exponent-part [float-suffix]
fractional-constant ::= [ digit ] ... . digit [ digit ] ...
                   | digit [ digit ] ... .
exponent-part     ::= exponent-indicator [ sign ] digit [ digit ] ...
exponent-indicator  ::= e | E
sign                ::= - | +
float-suffix        ::= f | F | l | L
character-constant ::= [ L ] ' char-const-char '
char-const-char ::= normal-char | std-esc | "
normal-char ::= any character except ', ", \ or a newline
std-esc ::= \n               // newline           LF
      | \t                     // horizontal tab    HT
      | \v                     // vertical tab      VT
      | \b                     // backspace         BS
      | \r                     // carriage return   CR
      | \f                     // form feed         FF
      | \a                     // alert             BEL
      | \\                     // backslash         \ 
      | \?                     // question mark     ? 
      | \'                     // single quote      ' 
      | \"                     // double quote      "
      | \ octal-code         // octal code        o, oo, ooo
      | \x hex-digit [ hex-digit ] ...   // hex code  xhh...
octal-code ::= octal-digit | octal-digit octal-digit
                 | octal-digit octal-digit octal-digit
string-literal ::= [ L ] " [ string-character ] ... "
string-character ::= normal-char | escape-sequence | '
escape-sequence ::= std-esc | non-std-esc
non-std-esc ::= \ non-escape-code
non-escape-code::= any character that cannot follow \ in a std-esc
abstract-string-literal ::= A " [ string-character ] ... "
lsl-constant ::= decimal-constant | character-constant

11.14 Declarations

declaration ::= [ decl-specifier-seq ] [ init-declarator-list ] ; [ fun-spec-body ]
         | [ decl-specifier-seq ] ctor-declarator [ fun-spec-body ]
         | block-declaration
         | function-definition
         | template-declaration
         | explicit-instantiation
         | explicit-specialization
         | linkage-declaration
         | namespace-definition
         | refinement-declaration
         | extern everything ;
block-declaration ::= asm-definition
         | namespace-alias-definition
         | using-declaration
         | using-directive
init-declarator-list ::= init-declarator [ , init-declarator ] ...
init-declarator ::= declarator [ initializer ]
initializer ::= = constant-expression | = { initializer-list }
      | ( expression-list )
constant-expression ::= exactly as in C++
initializer-list ::= initializer-clause [ , initializer-clause ] ... [ , ]
initializer-clause ::= assignment-expression
      | { [ initializer-list ] }
assignment-expression ::= exactly as in C++
expression-list ::= expression [ , expression ] ...
expression ::= exactly as in C++
decl-specifier ::= storage-class-specifier
         | type-specifier | function-specifier
         | friend | typedef
decl-specifier-seq ::= decl-specifier [ decl-specifier ] ...
storage-class-specifier ::= static | extern | mutable
        | auto | register
function-specifier ::= virtual | inline | explicit
type-specifier-seq ::= type-specifier [ type-specifier ] ...
type-specifier ::= simple-type-name
        | enum-specifier | class-specifier
        | elaborated-type-specifier | cv-qualifier
cv-qualifier ::=  const | volatile
simple-type-name ::= complete-type-name 
        | [ :: ] nested-name-specifier template template-class-instance
        | built-in-type-name
complete-type-name ::= complete-class-name
        | complete-non-class-type-name
complete-non-class-type-name ::=  [ :: ] [ nested-name-specifier ] non-class-type-name
non-class-type-name ::= enum-name | typedef-non-class-or-enum-name
built-in-type-name ::= char | short | int | long | signed | unsigned | float | double
        | bool | void
enum-name ::= original-enum-name | typedef-enum-name
complete-class-name ::= [ :: ] [ nested-name-specifier ] class-name
complete-namespace-name ::= [ :: ] [ nested-name-specifier ] namespace-name
nested-name-specifier ::= class-name :: | namespace-name ::
        | nested-name-specifier class-name ::
        | nested-name-specifier namespace-name ::
        | nested-name-specifier template template-class-instance ::
class-name ::= original-class-name | typedef-class-name | template-class-instance
namespace-name ::= original-namespace-name | namespace-alias-name
elaborated-type-specifier ::= class-key [ :: ] [ nested-name-specifier ] identifier
        | enum [ :: ] [ nested-name-specifier ] identifier
        | typename [ :: ] nested-name-specifier identifier
        | typename [ :: ] nested-name-specifier [ template ] template-class-instance
class-key ::= class | struct | union | signature
enum-specifier ::= enum [ identifier ] { [ enumerator-definition-list ] }
enumerator-definition-list ::= enumerator-definition [ , enumerator-definition ] ...
enumerator-definition ::= identifier [ constant-initializer ]
declarator ::= direct-declarator | ptr-operator declarator
direct-declarator ::= id-expression | direct-declarator declarator-qualifier
        | ( declarator )
declarator-qualifier ::= [ [ constant-expression ] ] | param-qualifier
param-qualifier ::= ( [ parameter-declaration-clause ] [ expects-clause ] )
id-expression ::= unqualified-id | qualified-id
unqualified-id ::= identifier
        | operator-function-id | conversion-function-id
        | template-instance
qualified-id ::= nested-name-specifier [ template ] unqualified-id
operator-function-id ::= operator C++-operator-symbol
conversion-function-id ::= operator type-specifier-seq [ ptr-operator ]
conversion-type-id ::= type-specifier-seq [ conversion-declarator ]
conversion-declarator ::= ptr-operator [ conversion-declarator ]
ptr-operator ::= * [ cv-qualifier-seq ] | &
      | [ :: ] nested-name-specifier * [ cv-qualifier-seq ]
cv-qualifier-seq ::= cv-qualifier [ cv-qualifier ] ...
abstract-declarator ::= ptr-operator [ abstract-declarator ]
      | direct-abstract-declarator
direct-abstract-declarator ::= [ direct-abstract-declarator ] declarator-qualifier
      | ( abstract-declarator )
function-definition ::= fun-interface [ fun-spec-body ] [ ctor-initializer ] fun-body
        | fun-interface [ fun-spec-body ] function-try-block
fun-interface ::= [ decl-specifier-seq ] declarator
        | [ decl-qualifier-seq ] ctor-declarator
        | [ decl-qualifier-seq ] special-function-declarator
decl-qualifier ::= storage-class-specifier | function-specifier | friend | typedef
decl-qualifier-seq ::= decl-qualifier [ decl-qualifier ] ...
ctor-initializer ::= : mem-initializer [ , mem-initializer ] ...
mem-initializer ::= mem-initializer-id ( expression-list )
mem-initializer-id ::= complete-class-name | identifier
expression-list ::= expression [ , expression ] ...
expression ::= exactly as in C++, but add the following
postfix-expression ::= postfix-expression ( [ expression-list ] [ using-trait-list ] )
    | simple-type-name ( [ expression-list ] [ using-trait-list ] )
function-try-block ::= try [ ctor-initializer ] fun-body handler-seq
handler-seq ::= handler [ handler ] ...
handler ::= catch ( exception-declaration ) compound-statement
exception-declaration ::= type-specifier-seq declarator
        | type-specifier-seq [ abstract-declarator ]
        | `...'
compound-statement ::= { statement-seq }
statement-seq ::= statement [ statement ] ...
statement ::= as in C++, but add ...
        | specification-statement
        | annotated-iteration-statement
ctor-declarator ::= complete-class-name param-qualifier
        | complete-template-class-name param-qualifier
complete-template-class-name ::= [ :: ] [ nested-name-specifier ] template-class-name
special-function-declarator ::= [ :: ] nested-name-specifier dtor-name param-qualifier
        | dtor-name param-qualifier | declarator-id param-qualifier
dtor-name ::= ~ original-class-name | ~ template-class-name
fun-body ::= compound-statement
parameter-declaration-clause ::= parameter-declaration-list [ `...' ]
        | `...' | parameter-declaration-list , `...'
parameter-declaration-list ::= parameter-declaration [ , parameter-declaration ] ...
parameter-declaration ::= decl-specifier-seq declarator [ parameter-initializer ]
        | decl-specifier-seq [ abstract-declarator ] [ parameter-initializer ]
parameter-initializer ::= = assignment-expression
assignment-expression ::= exactly as in C++
namespace-definition ::= namespace [ identifier ] { [ declaration-seq ] }
        | namespace original-namespace-name { [ declaration-seq ] }
declaration-seq ::= [ declaration-seq ] declaration
namespace-alias-definition ::= namespace identifier = complete-namespace-name ;
using-declaration ::= using qualified-id ;
        | using typename [ :: ] nested-name-specifier type-name ;
type-name ::= class-name | non-class-type-name|
using-directive ::= using namespace complete-namespace-name ;
linkage-declaration ::= extern string-literal { [ declaration-seq ] }
        | extern string-literal declaration
asm-definition ::= asm ( string-literal ) ;

11.15 Function Specifications

fun-spec-body ::= behavior { [ uses-seq ] [ declaration-seq ] spec-case-seq }
        | behavior program compound-statement
uses-seq ::= uses-clause [ uses-clause ] ...
spec-case-seq ::= spec-case [ also spec-case ] ...
spec-case ::= [ let-clause ] req-frame-ens [ example-seq ]
        | [ let-clause ] [ requires-clause-seq ] { spec-case-seq }  [ ensures-clause-seq ] [ example-seq ]
req-frame-ens ::= [ requires-clause-seq ] ensures-clause-seq
      | [ requires-clause-seq ] frame [ ensures-clause-seq ]
requires-clause-seq ::= requires-clause [ requires-clause ] ...
requires-clause ::= requires [ redundantly ] pre-cond ;
pre-cond ::= predicate
frame ::= accesses-clause-seq [ modifies-clause-seq ] [ trashes-clause-seq ] [ calls-clause-seq ]
        | modifies-clause-seq [ trashes-clause-seq ] [ calls-clause-seq ]
        | trashes-clause-seq [ calls-clause-seq ]
        | calls-clause-seq
ensures-clause-seq ::= ensures-clause [ ensures-clause ] ...
ensures-clause ::= ensures [ redundantly ] post-cond ;
         | ensures [ redundantly ] liberally post-cond ;
post-cond ::= predicate
predicate ::= term
term ::= if term then term else term
        | logical-term
logical-term ::= logical-term logical-opr equality-term
        | equality-term
logical-opr ::= \and  |  \or  |  \implies  |  /\  |  \/  |  =>
equality-term ::= lsl-op-term [ eq-opr lsl-op-term ]
        | quantifier [ quantifier ] ... ( term )
        | higher-order-comparison
        | informal-desc
eq-opr ::= = | == | \eq | ~= | != | \neq
quantifier ::= quantifier-sym quantified-list
quantifier-sym ::= \A | \forall | \E | \exists
quantified-list ::= varId : sort-name [ , varId : sort-name ] ...
varId ::= identifier
sort-name ::= identifier [ sort-instance-actuals ]
        | class-name | built-in-type-name
        | typedef-non-class-or-enum-name | typedef-enum-name
sort-instance-actuals ::= [ sort-or-type [ , sort-or-type ] ... ]
sort-or-type ::= identifier [ sort-instance-actuals ] | type-id
informal-desc ::= informally string-literal [ string-literal ] ...
      | informal-comment
lsl-op-term ::= lsl-op [ lsl-op ] ... secondary
        | secondary [ lsl-op secondary ] ...
        | secondary lsl-op [ lsl-op ] ...
secondary ::= primary | [ primary ] sc-bracketed [ : sort-name ] [ primary ]
sc-bracketed ::= [ [ term-list ] ] | { [ term-list ] }
        | \< [ term-list ] \> | \langle [ term-list ] \rangle
term-list ::= term [ , term ] ...
primary ::= primitive [ primary-suffix ] ...
primitive ::= ( term )
      | id-expression
      | fcnId ( term-list )
      | lcpp-primary
fcnId ::= identifier
primary-suffix ::= selection | : sort-name | state-function
selection ::= . identifier
lcpp-primary ::= literal | this | self | result
        | pre | post | any | returns
        | throws ( type-id )
        | thrown ( type-id )
        | sizeof ( type-id )
        | fresh ( term-list )
        | trashed ( store-ref-list )
        | unchanged ( store-ref-list )
state-function ::= ^ | \pre | ' | \post | \any | \obj
modifies-clause-seq ::= modifies-clause [ modifies-clause ] ...
modifies-clause ::= modifies [ redundantly ] store-ref-list ;
        | constructs [ redundantly ] store-ref-list ;
store-ref-list ::= store-ref [ , store-ref ] ... | nothing | everything
store-ref ::= term | reach ( term )
trashes-clause-seq ::= trashes-clause [ trashes-clause ] ...
trashes-clause ::= trashes [ redundantly ] store-ref-list ;
calls-clause-seq ::= calls-clause [ calls-clause ] ...
calls-clause ::= calls [ redundantly ] function-names ;
function-names ::= everything | nothing
       | function-name [ , function-name ] ...
function-name ::= term
accesses-clause-seq ::= accesses-clause [ accesses-clause ] ...
accesses-clause ::= accesses [ redundantly ] store-ref-list ;
let-clause ::= let be-list ;
be-list ::= varId : sort-name be term [ , varId : sort-name be term ] ...
example-seq ::= example [ example ] ...
example ::= example [ liberally ] predicate ;
exception-decl ::= throw ( [ type-list ] )
type-list ::= type-id [ , type-id ] ...
higher-order-comparison ::= lsl-op-term satisfies fun-interface fun-spec-body
expects-clause ::= expects expected-trait-list
expected-trait-list ::= trait [ simple-id ] [ , trait [ simple-id ] ] ...
using-trait-list ::= using trait-or-deref-list
trait-or-deref-list ::= trait
              | * simple-id
              | trait-or-deref-list , trait
              | trait-or-deref-list , * simple-id
specification-statement ::= fun-spec-body
     | requires-clause
     | accesses-clause
     | modifies-clause
     | trashes-clause
     | calls-clause
     | ensures-clause
     | assert [ redundantly ] predicate ;
     | assume-statement
     | nondeterministic-choice
     | nondeterministic-if
assume-statement ::= assume [ redundantly ] predicate ;
nondeterministic-choice ::= choose compound-statement [ or compound-statement ] ...
nondeterministic-if ::= if guarded-statement [ or guarded-statement ] ... [ else compound-statement ]
guarded-statement ::= { assume-statement [ statement-seq ] }
annotated-iteration-statement ::= [ maintaining-seq ] [ decreasing-seq ] iteration-statement
maintaining-seq ::= maintaining-clause [ maintaining-clause ] ...
maintaining-clause ::= maintaining [ redundantly ] predicate
decreasing-seq ::= decreasing-clause [ decreasing-clause ] ...
decreasing-clause ::= decreasing [ redundantly ] predicate
iteration-statement ::= a C++ while, do, or for statement

11.16 Class Specifications

class-specifier ::= class-head { [ member-seq ] }
class-head ::= class-key [ identifier ] [ base-spec ]
        | class-key nested-name-specifier identifier [ base-spec ]
        | class-key [ nested-name-specifier ] template-class-instance [ base-spec ]
        | abstract class [ nested-name-specifier ] [ identifier ] [ base-spec ]
member-seq ::= [ member-seq ] member-declaration
        | [ member-seq ] access-specifier :
        | [ member-seq ] larch-cpp-clause
larch-cpp-clause ::= uses-clause
        | simulates-clause
        | depends-clause
        | represents-clause
        | invariant-clause
        | constraint-clause
member-declaration ::= function-definition
        | [ decl-specifier-seq ] [ member-declarator-list ] ; [ fun-spec-body ]
        | [ decl-qualifier-seq ] ctor-declarator ; [ fun-spec-body ]
        | [ decl-qualifier-seq ] special-function-declarator ; [ fun-spec-body ]
        | [ :: ] nested-name-specifier [ template ] unqualified-id
        | using-declaration
        | template-declaration
        | spec-decl
        | refinement-member-decl
member-declarator-list ::= member-declarator [ , member-declarator ] ...
member-declarator ::= declarator [ constant-initializer ]
       | [ identifier ] : constant-expression
constant-initializer ::= = constant-expression
access-specifier ::= public | protected | private
invariant-clause ::= invariant [ redundantly ] predicate ;
constraint-clause ::= constraint [ redundantly ] predicate [ constrained-set ] ;
constrained-set ::= for fun-interface-list
fun-interface-list ::= fun-interface [ , fun-interface ] ...
        | nothing | everything
depends-clause ::= depends store-ref on store-ref-list ;
represents-clause ::= represents store-ref by predicate ;
base-spec ::= : base-list
base-list ::= base-specifier [ , base-specifier ] ...
base-specifier ::= [ virtual ] [ access-specifier ] complete-class-name
        | access-specifier [ virtual ] complete-class-name
simulates-clause ::= [ weakly ] simulates supertype-list ;
supertype-list ::= supertype [ , supertype ] ...
supertype ::= sort-name [ by fcnId ]

11.17 Template Specifications

template-declaration ::= [ export ] template < template-parameter-list [ expects-clause ] > 
template-parameter-list ::= template-parameter [ , template-parameter ] ...
template-parameter ::= type-parameter | parameter-declaration
type-parameter ::= class [ identifier ] [ type-init ] | typename [ identifier ] [ type-init ]
        | template < template-parameter-list [ expects-clause ] > class [ identifier ] [ template-init ]
type-init ::= = type-id
template-init ::= = complete-template-class-name | = complete-template-non-class-name
complete-template-non-class-name ::= [ :: ] [ nested-name-specifier ] template-non-class-name
where-seq ::= where-clause [ where-clause ] ...
where-clause ::= where type-arg-name is complete-class-name ;
      | where type-arg-name is where-body ;
where-body ::= [ class ] { member-seq }
type-arg-name ::= identifier | original-class-name | template-class-instance
template-instance ::= template-class-instance | template-non-class-instance
template-class-instance ::= template-class-name template-instance-actuals
template-non-class-instance ::= template-non-class-name template-instance-actuals
template-instance-actuals ::= < [ template-argument-list ] [ using-trait-list ] >
template-argument-list ::= template-argument [ , template-argument ] ...
template-argument ::= assignment-expression | type-id
        | [ :: ] [ nested-name-specifier ] template-class-name
        | [ :: ] [ nested-name-specifier ] template-non-class-name
type-id ::= type-specifier-seq [ abstract-declarator ]
explicit-instantiation ::= template declaration
explicit-specialization ::= template < > declaration

11.18 Specification Modules

interface ::= top-level [ top-level ] ...
top-level ::= uses-clause | spec-decl | depends-clause
        | represents-clause | invariant-clause | constraint-clause
        | declaration | using-declaration | using-directive
spec-decl ::= spec declaration
uses-clause ::= uses trait-list ;
trait-list ::= trait [ , trait ] ...
trait ::= trait-name [ ( renaming ) ]
trait-name ::= simple-id
renaming ::= replace-list | lsl-sort-list [ , replace-list ]
replace-list ::= replace [ , replace ] ...
replace ::= lsl-sort for lsl-formal
lsl-sort-list ::= lsl-sort [ , lsl-sort ]
lsl-sort ::= simple-id [ lsl-instance-actuals ]
               | built-in-type-name
               | lsl-constant
lsl-instance-actuals ::= [ lsl-sort-list ]
               | < lsl-sort-list >
lsl-formal ::= lsl-sort
               | simple-id [ : lsl-signature ]
lsl-signature ::= [ lsl-sort-list ] -> lsl-sort

11.19 Refinement

refinement-declaration ::= [ refine-prefix ] declaration
refine-prefix ::= refine refinable-id [ with replace-list ] by
refinable-id ::= original-class-name | typedef-class-name
      | class-key identifier
      | unqualified-id 
      | template-class-name | template-non-class-name
      | original-namespace-name | namespace-alias-name
refinement-member-decl ::= [ refine-prefix ] member-declaration

Go to the first, previous, next, last section, table of contents.