[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

C. Grammar Summary

The following is a summary of the context-free grammar for JML. 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.


C.1 Lexical Conventions

 
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 *


C.2 Compilation Units

 
compilation-unit ::= [ package-declaration ]
              [ import-declaration ] ...
              [ top-level-declaration ] ...
top-level-declaration ::= type-declaration
package-declaration ::= [ java-annotations ] package name ;
name ::= ident  [ . ident ] ...
import-declaration ::= [ model ] import [ static ] name-star ;
name-star ::= ident [ . ident ] ... [ . * ]


C.3 Type Declarations

 
type-declaration ::= class-declaration
        | interface-declaration
        | ;
class-declaration ::= [ doc-comment ] modifiers class ident
            [ class-extends-clause ] [ implements-clause ]
            class-block
class-block ::= { [ field ] ... }
interface-declaration ::= [ doc-comment ] modifiers interface ident
           [ interface-extends ]
           class-block
class-extends-clause ::= [ extends name ]
implements-clause ::= implements name-list
name-list ::= name [ , name ] ...
interface-extends ::= extends name-list
modifiers ::= [ modifier ] ...
modifier ::= public | protected | private
        | abstract | static |
        | final | synchronized
        | transient | volatile
        | native | strictfp
        | const             // reserved but not used in Java
        | java-annotation
        | jml-modifier
jml-modifier ::= spec_public | spec_protected
        | model | ghost | pure
        | instance | helper
        | uninitialized
        | spec_java_math | spec_safe_math | spec_bigint_math
        | code_java_math | code_safe_math | code_bigint_math
        | non_null | nullable | nullable_by_default
        | extract
java-annotations ::= java-annotation [ java-annotation ] ...
java-annotation ::= @ name ( [ element-value-pairs ] ... )
        | @ name
        | @ name ( element-values )
element-value-pairs ::= element-value [ , element-value ]
element-value-pair ::= ident = element-value
element-value ::= conditional-expr
        | annotation
        | element-value-array-initializer
element-value-array-initializer ::= `{' element-values ] `}'
element-values ::= element-value [ , element-value ] ... [ , ]


C.4 Class and Interface Member Declarations

 
field ::= member-decl
        | jml-declaration
        | class-initializer-decl
        | ;
member-decl ::= method-decl
        | variable-definition
        | class-declaration
        | interface-declaration
method-decl ::= [ doc-comment ] ...
                method-specification
                modifiers [ method-or-constructor-keyword ]
                [ type-spec ] method-head
                method-body
        | [ doc-comment ] ...
          modifiers [ method-or-constructor-keyword ]
          [ type-spec ] method-head
          [ method-specification ]
          method-body
method-or-constructor-keyword ::= method | constructor
method-head ::= ident formals [ dims ] [ throws-clause ]
method-body ::= compound-statement | ;
throws-clause ::= throws name [ , name ] ...
formals ::= ( [ param-declaration-list ] )
param-declaration-list ::= param-declaration
                           [ , param-declaration ] ...
param-declaration ::= [ param-modifier ] ... type-spec ident [ dims ]
param-modifier ::= final | non_null | nullable
variable-definition ::= [ doc-comment ] ... modifiers variable-decls
variable-decls ::= [ field ] type-spec variable-declarators ;
                   [ jml-data-group-clause ] ...
variable-declarators ::= variable-declarator
                         [ , variable-declarator ] ...
variable-declarator ::= ident [ dims ] [ = initializer ]
initializer ::= expression | array-initializer
array-initializer ::= { [ initializer-list ] } 
initializer-list ::= initializer [ , initializer ] ... [ , ]
type-spec ::= [ ownership-modifiers ] type [ dims ]
         | \TYPE [ dims ]
type ::= reference-type | built-in-type
reference-type ::= name
dims ::= `[' `]' [ `[' `]' ] ...
class-initializer-decl ::= [ method-specification ]
                           [ static ] compound-statement
        | method-specification static_initializer 
        | method-specification initializer 


C.5 Type Specifications

 
jml-declaration ::= modifiers invariant
        | modifiers history-constraint
        | modifiers represents-clause
        | modifiers initially-clause 
        | modifiers monitors-for-clause
        | modifiers readable-if-clause
        | modifiers writable-if-clause
        | axiom-clause
invariant ::= invariant-keyword predicate ;
invariant-keyword ::= invariant | invariant_redundantly
history-constraint ::= constraint-keyword predicate
              [ for constrained-list ] ;
constraint-keyword ::= constraint | constraint_redundantly
constrained-list ::= method-name-list | \everything
method-name-list ::= method-name [ , method-name ] ...
method-name ::= method-ref [ ( [ param-disambig-list ] ) ] | method-ref-start . * 
method-ref ::= method-ref-start [ . method-ref-rest ] ...
        | new reference-type
method-ref-start ::=  super | this | ident
method-ref-rest ::=  this | ident
param-disambig-list ::= param-disambig [ , param-disambig ] ...
param-disambig ::= type-spec [ ident [ dims ] ]
represents-clause ::= represents-keyword store-ref-expression = spec-expression ;
        | represents-keyword store-ref-expression \such_that predicate ;
represents-keyword ::= represents | represents_redundantly
initially-clause ::= initially predicate ;
axiom-clause ::= axiom predicate ;
readable-if-clause ::= readable ident if predicate ;
writable-if-clause ::= writable ident if predicate ;
monitors-for-clause ::= monitors_for ident


C.6 Method Specifications

 
method-specification ::= specification | extending-specification
extending-specification ::= also specification
specification ::= spec-case-seq [ redundant-spec ]
              | redundant-spec
spec-case-seq ::= spec-case [ also spec-case ] ...
spec-case ::= lightweight-spec-case | heavyweight-spec-case
        | model-program
privacy ::= public | protected | private
lightweight-spec-case ::= generic-spec-case
generic-spec-case ::= [ spec-var-decls ]
                      spec-header
                      [ generic-spec-body ]
        | [ spec-var-decls ]
          generic-spec-body
generic-spec-body ::= simple-spec-body
        | {| generic-spec-case-seq |}
generic-spec-case-seq ::= generic-spec-case
                          [ also generic-spec-case ] ...
spec-header ::= requires-clause [ requires-clause ] ...
simple-spec-body ::= simple-spec-body-clause
                     [ simple-spec-body-clause ] ... 
simple-spec-body-clause ::= diverges-clause
        | assignable-clause | accessible-clause
        | captures-clause | callable-clause
        | when-clause | working-space-clause
        | duration-clause | ensures-clause
        | signals-only-clause | signals-clause
        | measured-clause 
heavyweight-spec-case ::= behavior-spec-case
        | exceptional-behavior-spec-case
        | normal-behavior-spec-case
behavior-spec-case ::= [ privacy ] [ code ] behavior-keyword
                       generic-spec-case
behavior-keyword ::= behavior | behaviour
normal-behavior-spec-case ::= [ privacy ] [ code ] normal-behavior-keyword
                              normal-spec-case
normal-behavior-keyword ::= normal_behavior | normal_behaviour
normal-spec-case ::= generic-spec-case
exceptional-behavior-spec-case ::= [ privacy ] [ code ] exceptional-behavior-keyword
                                   exceptional-spec-case
exceptional-behavior-keyword ::= exceptional_behavior | exceptional_behaviour
exceptional-spec-case ::= generic-spec-case
spec-var-decls ::= forall-var-decls [ old-var-decls ]
        | old-var-decls
forall-var-decls ::= forall-var-declarator [ forall-var-declarator ] ... 
forall-var-declarator ::= forall [ bound-var-modifiers ] type-spec quantified-var-declarator ;
old-var-decls ::= old-var-declarator [ old-var-declarator ] ...
old-var-declarator ::= old [ bound-var-modifiers ] type-spec spec-variable-declarators ;
requires-clause ::= requires-keyword pred-or-not ;
        | requires-keyword \same ;
requires-keyword ::= requires | pre 
        | requires_redundantly | pre_redundantly
pred-or-not ::= predicate | \not_specified
ensures-clause ::= ensures-keyword pred-or-not ;
ensures-keyword ::= ensures | post
        | ensures_redundantly | post_redundantly
signals-clause ::= signals-keyword ( reference-type [ ident ] )
                   [ pred-or-not ] ;
signals-keyword ::= signals | signals_redundantly
        | exsures | exsures_redundantly
signals-only-clause ::= signals-only-keyword reference-type [ , reference-type ] ... ;
        | signals-only-keyword \nothing ;
signals-only-keyword ::= signals_only | signals_only_redundantly
diverges-clause ::= diverges-keyword pred-or-not ;
diverges-keyword ::= diverges | diverges_redundantly
when-clause ::= when-keyword pred-or-not ;
when-keyword ::= when | when_redundantly
assignable-clause ::= assignable-keyword store-ref-list ;
assignable-keyword ::= assignable | assignable_redundantly
        | modifiable | modifiable_redundantly
        | modifies | modifies_redundantly
accessible-clause ::= accessible-keyword store-ref-list ;
accessible-keyword ::= accessible | accessible_redundantly
callable-clause ::= callable-keyword callable-methods-list ;
callable-keyword ::= callable | callable_redundantly
callable-methods-list ::= method-name-list | store-ref-keyword
measured-clause ::= measured-by-keyword \not_specified ;
        | measured-by-keyword spec-expression [ if predicate ] ;
measured-by-keyword ::= measured_by | measured_by_redundantly
captures-clause ::= captures-keyword store-ref-list ;
captures-keyword ::= captures | captures_redundantly
working-space-clause ::= working-space-keyword \not_specified ;
        | working-space-keyword spec-expression [ if predicate ] ;
working-space-keyword ::= working_space | working_space_redundantly
duration-clause ::= duration-keyword \not_specified ;
        | duration-keyword spec-expression [ if predicate ] ;
duration-keyword ::= duration | duration_redundantly


C.7 Data Groups

 
jml-data-group-clause ::= in-group-clause | maps-into-clause
in-group-clause ::= in-keyword group-list ; 
in-keyword ::= in | in_redundantly
group-list ::= group-name [ , group-name ] ...
group-name ::= [ group-name-prefix ] ident 
group-name-prefix ::= super . | this . 
maps-into-clause ::= maps-keyword member-field-ref \into group-list ; 
maps-keyword ::= maps | maps_redundantly
member-field-ref ::= ident . maps-member-ref-expr
          | maps-array-ref-expr [ . maps-member-ref-expr ]
maps-member-ref-expr ::= ident | * 
maps-array-ref-expr ::= ident maps-spec-array-dim
                        [ maps-spec-array-dim ] ... 
maps-spec-array-dim ::= `[' spec-array-ref-expr `]'


C.8 Specification Inheritance

 


C.9 Predicates and Specification Expressions

 
predicate ::= spec-expression
spec-expression-list ::= spec-expression
                         [ , spec-expression ] ...
spec-expression ::= expression 
expression-list ::= expression [ , expression ] ...
expression ::= assignment-expr 
assignment-expr ::= conditional-expr
                    [ assignment-op assignment-expr ]
assignment-op ::=  = | += | -= | *= | /= | %= | >>=  
        | >>>= | <<= | &= | `|=' | ^=
conditional-expr ::= equivalence-expr
                   [ ? conditional-expr : conditional-expr ]
equivalence-expr ::= implies-expr
                     [ equivalence-op implies-expr ] ...
equivalence-op ::= <==> | <=!=>
implies-expr ::= logical-or-expr
             [ ==> implies-non-backward-expr ]
        | logical-or-expr <== logical-or-expr
             [ <== logical-or-expr ] ...
implies-non-backward-expr ::= logical-or-expr
             [ ==> implies-non-backward-expr ]
logical-or-expr ::= logical-and-expr [ `||' logical-and-expr ] ...
logical-and-expr ::= inclusive-or-expr [ && inclusive-or-expr ] ...
inclusive-or-expr ::= exclusive-or-expr [ `|' exclusive-or-expr ] ...
exclusive-or-expr ::= and-expr [ ^ and-expr ] ...
and-expr ::= equality-expr [ & equality-expr ] ...
equality-expr ::= relational-expr [ == relational-expr] ...
        | relational-expr [ != relational-expr] ...
relational-expr ::= shift-expr < shift-expr
        | shift-expr > shift-expr
        | shift-expr <= shift-expr
        | shift-expr >= shift-expr
        | shift-expr <: shift-expr
        | shift-expr [ instanceof type-spec ]
shift-expr ::= additive-expr [ shift-op additive-expr ] ...
shift-op ::= << | >> | >>>
additive-expr ::= mult-expr [ additive-op mult-expr ] ...
additive-op ::= + | -
mult-expr ::= unary-expr [ mult-op unary-expr ] ...
mult-op ::= * | / | %
unary-expr ::= ( type-spec ) unary-expr
        | ++ unary-expr
        | -- unary-expr
        | + unary-expr
        | - unary-expr
        | unary-expr-not-plus-minus
unary-expr-not-plus-minus ::= ~ unary-expr
        | ! unary-expr
        | ( built-in-type ) unary-expr
        | ( reference-type ) unary-expr-not-plus-minus
        | postfix-expr
postfix-expr ::= primary-expr [ primary-suffix ] ... [ ++ ]
        | primary-expr [ primary-suffix ] ... [ -- ]
        | built-in-type [ `[' `]' ] ... . class
primary-suffix ::= . ident
        | . this
        | . class
        | . new-expr
        | . super ( [ expression-list ] )
        | ( [ expression-list ] )
        | `[' expression `]'
        | [ `[' `]' ] ... . class
primary-expr ::= ident | new-expr 
        | constant | super | true
        | false | this | null
        | ( expression )
        | jml-primary
built-in-type ::= void | boolean | byte
        | char | short | int
        | long | float | double
constant ::= java-literal
new-expr ::= new type new-suffix
new-suffix ::= ( [ expression-list ] ) [ class-block ]
        | array-decl [ array-initializer ]
        | set-comprehension
array-decl ::= dim-exprs [ dims ]
dim-exprs ::= `[' expression `]' [ `[' expression `]' ] ...
array-initializer ::= { [ initializer [ , initializer ] ... [ , ] ] }
initializer ::= expression
        | array-initializer
jml-primary ::= result-expression
        | old-expression
        | not-assigned-expression
        | not-modified-expression
        | only-accessed-expression
        | only-assigned-expression
        | only-called-expression
        | only-captured-expression
        | fresh-expression
        | reach-expression
        | duration-expression
        | space-expression
        | working-space-expression
        | nonnullelements-expression
        | informal-description
        | typeof-expression
        | elemtype-expression
        | type-expression
        | lockset-expression
        | max-expression
        | is-initialized-expression
        | invariant-for-expression
        | lblneg-expression
        | lblpos-expression
        | spec-quantified-expr
result-expression ::= \result
old-expression ::= \old ( spec-expression [ , ident ] )
        | \pre ( spec-expression )
not-assigned-expression ::= \not_assigned ( store-ref-list )
not-modified-expression ::= \not_modified ( store-ref-list )
only-accessed-expression ::= \only_accessed ( store-ref-list )
only-assigned-expression ::= \only_assigned ( store-ref-list )
only-called-expression ::= \only_called ( method-name-list )
only-captured-expression ::= \only_captured ( store-ref-list )
fresh-expression ::= \fresh ( spec-expression-list )
reach-expression ::= \reach ( spec-expression )
duration-expression ::= \duration ( expression )
space-expression ::= \space ( spec-expression )
working-space-expression ::= \working_space ( expression )
nonnullelements-expression ::= \nonnullelements ( spec-expression )
typeof-expression ::= \typeof ( spec-expression )
elemtype-expression ::= \elemtype ( spec-expression )
type-expression ::= \type ( type )
lockset-expression ::= \lockset
max-expression ::= \max ( spec-expression )
is-initialized-expression ::= \is_initialized ( reference-type )
invariant-for-expression ::= \invariant_for ( spec-expression )
lblneg-expression ::= ( \lblneg ident spec-expression )
lblpos-expression ::= ( \lblpos ident spec-expression )
spec-quantified-expr ::= ( quantifier quantified-var-decls ;
                           [ [ predicate ] ; ]
                           spec-expression )
quantifier ::= \forall | \exists
        | \max | \min
        | \num_of | \product | \sum
quantified-var-decls ::= [ bound-var-modifiers ] type-spec quantified-var-declarator
                         [ , quantified-var-declarator ] ...
quantified-var-declarator ::= ident [ dims ]
spec-variable-declarators ::= spec-variable-declarator
                          [ , spec-variable-declarator ] ...
spec-variable-declarator ::= ident [ dims ]
                             [ = spec-initializer ]
spec-array-initializer ::= { [ spec-initializer
             [ , spec-initializer ] ... [ , ] ] }
spec-initializer ::= spec-expression
        | spec-array-initializer
bound-var-modifiers ::= non_null | nullable
set-comprehension ::= { [ bound-var-modifiers ] type-spec
            quantified-var-declarator `|'
            postfix-expr && predicate }
store-ref-list ::= store-ref-keyword | store-ref [ , store-ref ] ...
store-ref ::= store-ref-expression
        | informal-description 
store-ref-expression ::= store-ref-name [ store-ref-name-suffix ] ...
store-ref-name ::= ident | super | this
store-ref-name-suffix ::= . ident | . this | `[' spec-array-ref-expr `]' | . * 
spec-array-ref-expr ::= spec-expression
        | spec-expression .. spec-expression
        | *
store-ref-keyword ::= \nothing | \everything | \not_specified


C.10 Statements and Annotation Statements

 
compound-statement ::= { statement [ statement ] ... }
statement ::= compound-statement
        | local-declaration ;
        | ident : statement
        | expression ;
        | if ( expression )
          statement [ else statement ]
        | possibly-annotated-loop
        | break [ ident ] ;
        | continue [ ident ] ;
        | return [ expression ] ;
        | switch-statement
        | try-block 
        | throw expression ;
        | synchronized ( expression ) statement
        | ;
        | jml-annotation-statement
        | assert-statement
        | jml-annotation-statement
        | model-prog-statement // only allowed in model programs
switch-statement ::= switch ( expression ) {
                     [ switch-body ] ... }
switch-body ::= switch-label-seq [ statement ] ...
switch-label-seq ::= switch-label [ switch-label ] ...
switch-label ::= case expression : | default :
try-block ::= try compound-statement
              [ handler ] ...
              [ finally compound-statement ]
handler ::= catch ( param-declaration ) compound-statement
local-declaration ::= local-modifiers variable-decls
local-modifiers ::= [ local-modifier ] ...
local-modifier ::= ghost | final  uninitialized | non_null | nullable
         | ownership-modifier  // when the Universe type system is on
possibly-annotated-loop ::=
          [ loop-invariant ] ...
          [ variant-function ] ...
          [ ident : ] loop-stmt
loop-stmt ::= while ( expression ) statement
        | do statement while ( expression ) ;
        | for ( [ for-init ] ; [ expression ] ; [ expression-list ] )
             statement
        | for ( modifiers type-spec ident : expression ) 
              statement
for-init ::= local-declaration | expression-list
loop-invariant ::= maintaining-keyword predicate ;
maintaining-keyword ::= maintaining | maintaining_redundantly
        | loop_invariant | loop_invariant_redundantly
variant-function ::= decreasing-keyword spec-expression ;
decreasing-keyword ::= decreasing | decreasing_redundantly
        | decreases | decreases_redundantly
assert-statement ::= assert expression [ : expression ] ;
        | assert predicate [ : expression ] ;
assert-redundantly-statement ::= assert_redundantly predicate
                                 [ : expression ] ;
jml-annotation-statement ::= assert-redundantly-statement
        | assume-statement
        | hence-by-statement
        | set-statement
        | refining-statement
        | unreachable-statement
        | debug-statement
assume-statement ::= assume-keyword predicate
                     [ : expression ] ;
assume-keyword ::= assume | assume_redundantly
set-statement ::= set assignment-expr ;
refining-statement ::= refining spec-statement statement
        | refining generic-spec-statement-case statement
unreachable-statement ::= unreachable ;
debug-statement ::= debug expression ;
hence-by-statement ::= hence-by-keyword predicate ;
hence-by-keyword ::= hence_by | hence_by_redundantly


C.11 Redundancy

 
redundant-spec ::= implications [ examples ] | examples
implications ::= implies_that spec-case-seq
examples ::= for_example example [ also example ] ...
example ::= [ [ privacy ] example ]
            [ spec-var-decls ]
            [ spec-header ]
            simple-spec-body
        | [ privacy ] exceptional_example
          [ spec-var-decls ]
          spec-header
          [ exceptional-example-body ]
        | [ privacy ] exceptional_example
          [ spec-var-decls ]
          exceptional-example-body
        | [ privacy ] normal_example
          [ spec-var-decls ]
          spec-header
          [ normal-example-body ]
        | [ privacy ] normal_example
          [ spec-var-decls ]
          normal-example-body
exceptional-example-body ::= exceptional-spec-case
                             [ exceptional-spec-case ] ...
normal-example-body ::= normal-spec-case
                        [ normal-spec-case ] ...


C.12 Model Programs

 
model-program ::= [ privacy ] [ code ] model_program 
                  jml-compound-statement
jml-compound-statement ::= compound-statement
jml-statement ::= statement
model-prog-statement ::= nondeterministic-choice
        | nondeterministic-if
        | spec-statement
        | invariant
nondeterministic-choice ::= choose alternative-statements
alternative-statements ::= jml-compound-statement
             [ or jml-compound-statement ] ...
nondeterministic-if ::= choose_if guarded-statements
             [ else jml-compound-statement ]
guarded-statements ::= guarded-statement
             [ or guarded-statement ] ...
guarded-statement ::= {
             assume-statement
             jml-statement [ jml-statement] ... }
spec-statement ::= [ privacy ] behavior-keyword
                   generic-spec-statement-case
        | [ privacy ] exceptional-behavior-keyword
          exceptional-spec-case
        | [ privacy ] normal-behavior-keyword
          normal-spec-case
        | [ privacy ] abrupt-behavior-keyword
          abrupt-spec-case
generic-spec-statement-case ::= [ spec-var-decls ]
                                generic-spec-statement-body
        | [ spec-var-decls ]
          spec-header
          [ generic-spec-statement-body ]
generic-spec-statement-body ::= simple-spec-statement-body
        | {| generic-spec-statement-case-seq |}
generic-spec-statement-case-seq ::= generic-spec-statement-case
             [ also generic-spec-statement-case ] ...
simple-spec-statement-body ::= simple-spec-statement-clause
                               [ simple-spec-statement-clause ] ... 
simple-spec-statement-clause ::= diverges-clause
        | assignable-clause | accessible-clause 
        | captures-clause | callable-clause
        | when-clause | working-space-clause | duration-clause
        | ensures-clause | signals-only-clause | signals-clause
        | measured-clause
        | continues-clause | breaks-clause | returns-clause
abrupt-behavior-keyword ::= abrupt_behavior | abrupt_behaviour
abrupt-spec-case ::= generic-spec-statement-case
continues-clause ::= continues-keyword [ target-label ]
                     [ pred-or-not ] ;
continues-keyword ::= continues | continues_redundantly
target-label ::= -> ( ident )
breaks-clause ::= breaks-keyword [ target-label ]
                  [ pred-or-not ] ;
breaks-keyword ::= breaks | breaks_redundantly
returns-clause ::= returns-keyword [ pred-or-not ] ;
returns-keyword ::= returns | returns_redundantly


C.13 Specification for Subtypes

 


C.14 Separate Files for Specifications

 


C.15 Universe Type System

 
ownership-modifiers ::= ownership-modifier [ ownership-modifier ]
ownership-modifier ::= \rep | \peer | \readonly
         | reserved-ownership-modifier // with --universesx parse or --universesx full
reserved-ownership-modifier ::= rep | peer | readonly


C.16 Safe Math Extensions

 
annotation-marker ::= 
        | /*+@ [ @ ] ... 
        | //-@ [ @ ] ... 
        | /*-@ [ @ ] ... 
represents-clause ::= represents-keyword store-ref-expression <- spec-expression ;
monitors-for-clause ::= monitors_for ident
compilation-unit ::= [ package-declaration ]
              refine-prefix
              [ import-declaration ] ...
              [ top-level-declaration ] ...
refine-prefix ::= refine-keyword string-literal ;
refine-keyword ::= refine | refines


[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

This document was generated by U-leavens-nd\leavens on May, 31 2013 using texi2html