|
ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved |
||||||||||
PREV PACKAGE NEXT PACKAGE | FRAMES NO FRAMES |
Class Summary | |
ErrorPragmaParser | This class produces a PragmaParser that reports an
client-chosen error message each time an annotation comment is
encountered. |
EscPragmaLex | This lexer overrides Lex.scanJavaExtensions(int) to
support "informal predicates". |
EscPragmaParser | Grammar: Pragma ::= LexicalPragma | ModifierPragma | TypeDeclElemPragma | StmtPragma LexicalPragma ::= "nowarn" [ Idn [',' Idn]* ] [';'] StmtPragma ::= SimpleStmtPragma [';'] | ExprStmtPragma SpecExpr [';'] | 'set' PrimaryExpr '=' SpecExpr [';'] SimpleStmtPragma ::= 'unreachable' ExprStmtPragma ::= 'assume' | 'assume_redundantly' | 'assert' | 'assert_redundantly' | 'loop_inv' | 'loop_invariant' | 'loop_invariant_redundantly' | 'decreases' | 'decreases_redundantly' | 'loop_predicate' | 'maintaining' | 'maintaining_redundantly' | 'decreasing' | 'decreasing_redundantly' TypeDeclElemPragma ::= ExprDeclPragma SpecExpr [';'] | 'ghost' Modifiers Type VariableDeclarator [';'] | 'still_deferred' Idn [',' Idn]* [';'] ExprDeclPragma ::= 'axiom' | 'invariant' | 'invariant_redundantly' ModifierPragma ::= [PrivacyPragma] [BehaviorPragma] SimpleModifierPragma [PrivacyPragma] [BehaviorPragma] NonSimpleModifierPragma NonSimpleModifierPragma ::= | ['also'] ExprModifierPragma SpecExpr [';'] | ['also'] VarExprModifierPragma '(' Type Idn ')' SpecExpr [';'] | ['also'] 'monitored_by' SpecExpr [',' SpecExpr]* [';'] | ['also'] ModifierPragma SpecDesignator [',' SpecDesignator]* [';'] PrivacyPragma ::= 'public' | 'private' | 'protected' BehaviorPragma ::= 'behavior' | 'normal_behavior' | 'exceptional_behavior' SimpleModifierPragma ::= 'uninitialized' | 'monitored' | 'non_null' | 'instance' | 'pure' | 'spec_public' | 'writable_deferred' | 'helper' | 'public' | 'private' | 'protected' | 'spec_protected' | 'model' | 'transient' | '\peer' | '\readonly' | '\rep' | 'may_be_null' | 'non_null_ref_by_default' | 'null_ref_by_default' | 'obs_pure' | 'code_java_math' | 'code_safe_math' | 'code_bigint_math' | 'spec_java_math' | 'spec_safe_math' | 'spec_bigint_math' ExprModifierPragma ::= 'readable_if' | 'writable_if' | 'requires' | 'requires_redundantly' | 'also_requires' (if Main.allowAlsoRequires) | 'ensures' | 'ensures_redundantly' | 'also_ensures' | 'pre' | 'pre_redundantly' | 'post' | 'post_redundantly' VarExprModifierPragma ::= 'exsures' | 'exsures_redundantly' | 'also_exsures" | 'signals' | 'signals_redundantly' ModifierPragma ::= 'modifies' | 'modifies_redundantly' | 'also_modifies' | 'modifiable' | 'modifiable_redundantly' | 'assignable' | 'assignable_redundantly' DurationClause ::= DurationKeyword '\not_specified' ';' | DurationKeyword DurSpecExpr [ 'if' predicate ] ';' DurSpecExpr ::= SpecExpr (of type long) OpWithLongResult DurSpecExpr | '\duration' '(' MethodInvOrConstructor ')' LongOp DurSpecExpr; MethodInvOrConstructorOrNotSpecified ::= MethodInvOrConstructor | '\not_specified'; InvariantForExpr ::= '\invariant_for' '(' SpecExpr ')' ';' SpaceExpr ::= '\space' '(' SpecExpr ')' IsInitializedExpr ::= '\is_initialized' '(' Idn ')' ';' InvariantFor ::= '\invariant_for' '(' SpecExpr ')' ';' WorkingSpaceClause ::= WorkingSpaceKeyword '\not_specified' ';' | WorkingSpaceKeyword WorkingSpaceSpecExpr [ 'if' predicate ] ';' WorkingSpaceSpecExpr ::= SpecExpr (of type int) OpWithIntResult WorkingSpaceSpecExpr | '\working_space' '(' MethodInvOrConstructor ')' IntOp WorkingSpaceSpecExpr MethodInvOrConstructor ::= MethodInvocation | ConstructorInvocation OpWithIntResult ::= STAR | '/' | '%' | PLUS | '-' | '&' | BITOR | '^' WorkingSpaceKeyword ::= 'working_space' | 'working_space_redundantly' DurationKeyword ::= 'duration' | 'duration_redundantly' PrivateDataKeyword ::= '\private_data' NotModifiedExpr ::= '\not_modified' '(' SpecDesignator [',' SpecDesignator]* ')' ';' ReachExpr ::= '\reach' '(' SpecExpr [ ',' Idn [ ',' StoreRefExpr ] ] ')' ';' FieldsOfExpr ::= '\fields_of' '(' SpecExpr [ ',' Idn [ ',' StoreRefExpr ] ] ')' ';' OtherExpr ::= '\other' [ StoreRefNameSuffix ] ';' ReachExpr ::= '\reach' '(' SpecExpr [ ',' Idn [ ',' StoreRefExpr ] ] ')' ';' StoreRefList ::= StoreRef [ ',' StoreRef ] ... |
JmlCorrelatedReader | This FilterCorrelatedReader creates the illusion that the
additional \@-signs, etc. allowed in the JML annotation syntax are
really just whitespace. |
OldVarDecl |
|
ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved |
||||||||||
PREV PACKAGE NEXT PACKAGE | FRAMES NO FRAMES |