| |
microsyntax ::= lexeme [ lexeme ] ...
lexeme ::= white-space | lexical-pragma | comment
| annotation-marker | doc-comment | token
token ::= ident | keyword | special-symbol
| java-literal | informal-description
white-space ::= non-nl-white-space | end-of-line
non-nl-white-space ::= a blank, tab, or formfeed character
end-of-line ::= newline | carriage-return
| carriage-return newline
newline ::= a newline character
carriage-return ::= a carriage return character
lexical-pragma ::= nowarn-pragma
nowarn-pragma ::= nowarn [ spaces ] [ nowarn-label-list ] ;
spaces ::= non-nl-white-space [ non-nl-white-space ] ...
nowarn-label-list ::= nowarn-label [ spaces ]
[ , [ spaces ] nowarn-label [ spaces ] ] ...
nowarn-label ::= letter [ letter ] ...
comment ::= C-style-comment | C++-style-comment
C-style-comment ::= /* [ C-style-body ] C-style-end
C-style-body ::= non-at-plus-minus-star [ non-stars-slash ] ...
| + non-letter [ non-stars-slash ] ...
| - non-letter [ non-stars-slash ] ...
| stars-non-slash [ non-stars-slash ] ...
non-letter ::= any character except _, a through z, or A through Z
non-stars-slash ::= non-star
| stars-non-slash
stars-non-slash ::= * [ * ] ... non-star-slash
non-at-plus-minus-star ::= any character except @, +, -, or *
non-star ::= any character except *
non-slash ::= any character except /
non-star-slash ::= any character except * or /
C-style-end ::= [ * ] ... */
C++-style-comment ::= // [ + ] end-of-line
| // non-at-plus-minus-end-of-line [ non-end-of-line ] ... end-of-line
| //+ non-letter-end-of-line [ non-end-of-line ] ... end-of-line
| //- non-letter-end-of-line [ non-end-of-line ] ... end-of-line
non-letter-end-of-line ::= any character except _, a through z, A through Z, a newline, or a carriage return
non-end-of-line ::= any character except a newline or carriage return
non-at-plus-minus-end-of-line ::= any character except @, +,-, newline, or carriage return
non-at-end-of-line ::= any character except @, newline, or carriage return
annotation-marker ::=
| /* [ annotation-key ]... @ [ ignored-at-in-annotation ] ...
| [ ignored-at-in-annotation ] ... @+*/
| [ ignored-at-in-annotation ] ... */
annotation-key ::= positive-key | negative-key
positive-key ::= + ident
negative-key ::= - ident
ignored-at-in-annotation ::= @
doc-comment ::= /** [ * ] ... doc-comment-body [ * ] ... */
doc-comment-ignored ::= doc-comment
doc-comment-body ::= [ description ] ...
[ tagged-paragraph ] ...
[ jml-specs ] [ description ]
description ::= doc-non-empty-textline
tagged-paragraph ::= paragraph-tag [ doc-non-nl-ws ] ...
[ doc-atsign ] ... [ description ] ...
jml-specs ::= jml-tag [ method-specification ] end-jml-tag
[ jml-tag [ method-specification ] end-jml-tag ] ...
paragraph-tag ::= @author | @deprecated | @exception
| @param | @return | @see
| @serial | @serialdata | @serialfield
| @since | @throws | @version
| @ letter [ letter ] ...
doc-atsign ::= @
doc-nl-ws ::= end-of-line
[ doc-non-nl-ws ] ... [ * [ * ] ... [ doc-non-nl-ws ] ... ]
doc-non-nl-ws ::= non-nl-white-space
doc-non-empty-textline ::= non-at-end-of-line [ non-end-of-line ] ...
jml-tag ::= <jml> | <JML> | <esc> | <ESC>
end-jml-tag ::= </jml> | </JML> | </esc> | </ESC>
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
keyword ::= java-reserved-word
| jml-predicate-keyword | jml-keyword
java-reserved-word ::= abstract | assert
| boolean | break | byte
| case | catch | char
| class | const | continue
| default | do | double
| else | extends | false
| final | finally | float
| for | goto | if
| implements | import | instanceof
| int | interface | long
| native | new | null
| package | private | protected
| public | return | short
| static | strictfp | super
| switch | synchronized | this
| throw | throws | transient
| true | try | void
| volatile | while
| java-universe-reserved // When the Universe option is on
java-universe-reserved ::= peer | pure
| readonly | rep
jml-predicate-keyword ::= \TYPE
| \bigint | \bigint_math | \duration
| \elemtype | \everything | \exists
| \forall | \fresh
| \into | \invariant_for | \is_initialized
| \java_math | \lblneg | \lblpos
| \lockset | \max | \min
| \nonnullelements | \not_assigned
| \not_modified | \not_specified
| \nothing | \nowarn | \nowarn_op
| \num_of | \old | \only_accessed
| \only_assigned | \only_called
| \only_captured | \pre
| \product | \reach | \real
| \result | \same | \safe_math
| \space | \such_that | \sum
| \typeof | \type | \warn_op
| \warn | \working_space
| jml-universe-pkeyword
jml-universe-pkeyword ::= \peer | \readonly | \rep
jml-keyword ::= abrupt_behavior | abrupt_behaviour
| accessible | accessible_redundantly
| also | assert_redundantly
| assignable | assignable_redundantly
| assume | assume_redundantly | axiom
| behavior | behaviour
| breaks | breaks_redundantly
| callable | callable_redundantly
| captures | captures_redundantly
| choose | choose_if
| code | code_bigint_math |
| code_java_math | code_safe_math
| constraint | constraint_redundantly
| constructor | continues | continues_redundantly
| decreases | decreases_redundantly
| decreasing | decreasing_redundantly
| diverges | diverges_redundantly
| duration | duration_redundantly
| ensures | ensures_redundantly | example
| exceptional_behavior | exceptional_behaviour
| exceptional_example
| exsures | exsures_redundantly | extract
| field | forall
| for_example | ghost
| helper | hence_by | hence_by_redundantly
| implies_that | in | in_redundantly
| initializer | initially | instance
| invariant | invariant_redundantly
| loop_invariant | loop_invariant_redundantly
| maintaining | maintaining_redundantly
| maps | maps_redundantly
| measured_by | measured_by_redundantly
| method | model | model_program
| modifiable | modifiable_redundantly
| modifies | modifies_redundantly
| monitored | monitors_for | non_null
| normal_behavior | normal_behaviour
| normal_example | nowarn
| nullable | nullable_by_default
| old | or
| post | post_redundantly
| pre | pre_redundantly
| pure | readable
| refining
| represents | represents_redundantly
| requires | requires_redundantly
| returns | returns_redundantly
| set | signals | signals_only
| signals_only_redundantly | signals_redundantly
| spec_bigint_math | spec_java_math
| spec_protected | spec_public | spec_safe_math
| static_initializer | uninitialized | unreachable
| when | when_redundantly
| working_space | working_space_redundantly
| writable
| jml-universe-keyword
jml-universe-keyword ::= peer | readonly | rep
special-symbol ::= java-special-symbol | jml-special-symbol
java-special-symbol ::= java-separator | java-operator
java-separator ::= ( | ) | { | } | `[' | `]' | ; | , | . | @
java-operator ::= = | < | > | ! | ~ | ? | :
| == | <= | >= | != | && | `||' | ++ | --
| + | - | * | / | & | `|' | ^ | % | << | >> | >>>
| += | -= | *= | /= | &= | `|=' | ^= | %=
| <<= | >>= | >>>=
jml-special-symbol ::= ==> | <== | <==> | <=!=>
| -> | <- | <: | .. | `{|' | `|}'
| <# | <#=
java-literal ::= integer-literal
| floating-point-literal | boolean-literal
| character-literal | string-literal | null-literal
integer-literal ::= decimal-integer-literal
| hex-integer-literal | octal-integer-literal
decimal-integer-literal ::= non-zero-digit [ digits ] [ integer-type-suffix ]
digits ::= digit [ digit ] ...
digit ::= 0 | non-zero-digit
non-zero-digit ::= 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9
integer-type-suffix ::= l | L
hex-integer-literal ::= hex-numeral [ integer-type-suffix ]
hex-numeral ::= 0x hex-digit [ hex-digit ] ...
| 0X hex-digit [ hex-digit ] ...
hex-digit ::= digit | a | b | c | d | e | f
| A | B | C | D | E | F
octal-integer-literal ::= octal-numeral [ integer-type-suffix ]
octal-numeral ::= 0 octal-digit [ octal-digit ] ...
octal-digit ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7
floating-point-literal ::= digits . [ digits ]
[ exponent-part ] [ float-type-suffix ]
| . digits [ exponent-part ] [ float-type-suffix ]
| digits exponent-part [ float-type-suffix ]
| digits [ exponent-part ] float-type-suffix
exponent-part ::= exponent-indicator signed-integer
exponent-indicator ::= e | E
signed-integer ::= [ sign ] digits
sign ::= + | -
float-type-suffix ::= f | F | d | D
boolean-literal ::= true | false
character-literal ::= ' single-character ' | ' escape-sequence '
single-character ::= any character except ', \, carriage return, or newline
escape-sequence ::= \b // backspace
| \t // tab
| \n // newline
| \r // carriage return
| \' // single quote
| \" // double quote
| \\ // backslash
| octal-escape
| unicode-escape
octal-escape ::= \ octal-digit [ octal-digit ]
| \ zero-to-three octal-digit octal-digit
zero-to-three ::= 0 | 1 | 2 | 3
unicode-escape ::= \u hex-digit hex-digit hex-digit hex-digit
string-literal ::= " [ string-character ] ... "
string-character ::= escape-sequence
| any character except ", \, carriage return, or newline
null-literal ::= null
informal-description ::= (* non-stars-close [ non-stars-close ] ... *)
non-stars-close ::= non-star
| stars-non-close
stars-non-close ::= * [ * ] ... non-star-close
non-star-close ::= any character except ) or *
|