org.jmlspecs.checker
Class JmlIDKeywords
java.lang.Object
org.jmlspecs.checker.JmlIDKeywords
- All Implemented Interfaces:
- JmlExprIDTokenTypes, JmlIDTokenTypes, JmlTopIDTokenTypes, MjcIDTokenTypes
- final class JmlIDKeywords
- extends Object
- implements JmlIDTokenTypes
| Fields inherited from interface org.jmlspecs.checker.JmlIDTokenTypes |
AFFIRM, BACKWARD_IMPLIES, EQUIV, IMPLIES, INFORMAL_DESC, L_ARROW, LCURLY_VBAR, LITERAL_abrupt_behavior, LITERAL_abrupt_behaviour, LITERAL_accessible, LITERAL_accessible_redundantly, LITERAL_also, LITERAL_assert_redundantly, LITERAL_assignable, LITERAL_assignable_redundantly, LITERAL_assume, LITERAL_assume_redundantly, LITERAL_axiom, LITERAL_behavior, LITERAL_behaviour, LITERAL_breaks, LITERAL_breaks_redundantly, LITERAL_callable, LITERAL_callable_redundantly, LITERAL_captures, LITERAL_captures_redundantly, LITERAL_choose, LITERAL_choose_if, LITERAL_code, LITERAL_code_bigint_math, LITERAL_code_contract, LITERAL_code_java_math, LITERAL_code_safe_math, LITERAL_constraint, LITERAL_constraint_redundantly, LITERAL_constructor, LITERAL_continues, LITERAL_continues_redundantly, LITERAL_debug, LITERAL_decreases, LITERAL_decreases_redundantly, LITERAL_decreasing, LITERAL_decreasing_redundantly, LITERAL_diverges, LITERAL_diverges_redundantly, LITERAL_duration, LITERAL_duration_redundantly, LITERAL_ensures, LITERAL_ensures_redundantly, LITERAL_example, LITERAL_exceptional_behavior, LITERAL_exceptional_behaviour, LITERAL_exceptional_example, LITERAL_exsures, LITERAL_exsures_redundantly, LITERAL_field, LITERAL_for_example, LITERAL_forall, LITERAL_ghost, LITERAL_helper, LITERAL_hence_by, LITERAL_hence_by_redundantly, LITERAL_implies_that, LITERAL_in, LITERAL_in_redundantly, LITERAL_initializer, LITERAL_initially, LITERAL_instance, LITERAL_invariant, LITERAL_invariant_redundantly, LITERAL_loop_invariant, LITERAL_loop_invariant_redundantly, LITERAL_maintaining, LITERAL_maintaining_redundantly, LITERAL_maps, LITERAL_maps_redundantly, LITERAL_measured_by, LITERAL_measured_by_redundantly, LITERAL_method, LITERAL_model, LITERAL_model_program, LITERAL_modifiable, LITERAL_modifiable_redundantly, LITERAL_modifies, LITERAL_modifies_redundantly, LITERAL_monitored, LITERAL_monitors_for, LITERAL_non_null, LITERAL_non_null_by_default, LITERAL_normal_behavior, LITERAL_normal_behaviour, LITERAL_normal_example, LITERAL_nullable, LITERAL_nullable_by_default, LITERAL_old, LITERAL_or, LITERAL_post, LITERAL_post_redundantly, LITERAL_pre, LITERAL_pre_redundantly, LITERAL_query, LITERAL_readable, LITERAL_refine, LITERAL_refines, LITERAL_represents, LITERAL_represents_redundantly, LITERAL_requires, LITERAL_requires_redundantly, LITERAL_returns, LITERAL_returns_redundantly, LITERAL_secret, LITERAL_set, LITERAL_signals, LITERAL_signals_only, LITERAL_signals_only_redundantly, LITERAL_signals_redundantly, LITERAL_spec_bigint_math, LITERAL_spec_java_math, LITERAL_spec_protected, LITERAL_spec_public, LITERAL_spec_safe_math, LITERAL_static_initializer, LITERAL_uninitialized, LITERAL_unreachable, LITERAL_weakly, LITERAL_when, LITERAL_when_redundantly, LITERAL_working_space, LITERAL_working_space_redundantly, LITERAL_writable, NOT_EQUIV, R_ARROW, SUBTYPE_OF, VBAR_RCURLY |
| Fields inherited from interface org.jmlspecs.checker.JmlExprIDTokenTypes |
LITERAL_BS_bigint, LITERAL_BS_bigint_math, LITERAL_BS_duration, LITERAL_BS_elemtype, LITERAL_BS_everything, LITERAL_BS_exists, LITERAL_BS_forall, LITERAL_BS_fresh, LITERAL_BS_into, LITERAL_BS_invariant_for, LITERAL_BS_is_initialized, LITERAL_BS_java_math, LITERAL_BS_lblneg, LITERAL_BS_lblpos, LITERAL_BS_lockset, LITERAL_BS_max, LITERAL_BS_min, LITERAL_BS_nonnullelements, LITERAL_BS_not_assigned, LITERAL_BS_not_modified, LITERAL_BS_not_specified, LITERAL_BS_nothing, LITERAL_BS_nowarn, LITERAL_BS_nowarn_op, LITERAL_BS_num_of, LITERAL_BS_old, LITERAL_BS_only_accessed, LITERAL_BS_only_assigned, LITERAL_BS_only_called, LITERAL_BS_only_captured, LITERAL_BS_other, LITERAL_BS_pre, LITERAL_BS_product, LITERAL_BS_reach, LITERAL_BS_real, LITERAL_BS_result, LITERAL_BS_safe_math, LITERAL_BS_same, LITERAL_BS_space, LITERAL_BS_such_that, LITERAL_BS_sum, LITERAL_BS_TYPE, LITERAL_BS_type, LITERAL_BS_typeof, LITERAL_BS_warn, LITERAL_BS_warn_op, LITERAL_BS_working_space, LITERAL_U_peer, LITERAL_U_readonly, LITERAL_U_rep |
| Fields inherited from interface org.multijava.mjc.MjcIDTokenTypes |
ASSIGN, AT, BAND, BAND_ASSIGN, BNOT, BOR, BOR_ASSIGN, BSR, BSR_ASSIGN, BXOR, BXOR_ASSIGN, CHARACTER_LITERAL, COLON, COMMA, DEC, DOT, EOF, EQUAL, GE, GT, IDENT, INC, INTEGER_LITERAL, JAVADOC_OPEN, LAND, LBRACK, LCURLY, LE, LITERAL__nowarn, LITERAL__nowarn_op, LITERAL__warn, LITERAL__warn_op, LITERAL_abstract, LITERAL_assert, LITERAL_boolean, LITERAL_break, LITERAL_byte, LITERAL_case, LITERAL_catch, LITERAL_char, LITERAL_class, LITERAL_const, LITERAL_continue, LITERAL_default, LITERAL_do, LITERAL_double, LITERAL_else, LITERAL_extends, LITERAL_false, LITERAL_final, LITERAL_finally, LITERAL_float, LITERAL_for, LITERAL_goto, LITERAL_if, LITERAL_implements, LITERAL_import, LITERAL_instanceof, LITERAL_int, LITERAL_interface, LITERAL_long, LITERAL_native, LITERAL_new, LITERAL_null, LITERAL_package, LITERAL_peer, LITERAL_private, LITERAL_protected, LITERAL_public, LITERAL_pure, LITERAL_readonly, LITERAL_rep, LITERAL_resend, LITERAL_return, LITERAL_short, LITERAL_static, LITERAL_strictfp, LITERAL_super, LITERAL_switch, LITERAL_synchronized, LITERAL_this, LITERAL_throw, LITERAL_throws, LITERAL_transient, LITERAL_true, LITERAL_try, LITERAL_void, LITERAL_volatile, LITERAL_while, LNOT, LOR, LPAREN, LT, MINUS, MINUS_ASSIGN, NOT_EQUAL, NULL_TREE_LOOKAHEAD, PERCENT, PERCENT_ASSIGN, PLUS, PLUS_ASSIGN, QUESTION, RBRACK, RCURLY, REAL_LITERAL, RPAREN, SEMI, SL, SL_ASSIGN, SLASH, SLASH_ASSIGN, SR, SR_ASSIGN, STAR, STAR_ASSIGN, STRING_LITERAL |
|
Method Summary |
private static boolean |
equals(char[] key,
int offset,
int length,
char[] word)
|
private static int |
find(char[] key,
int offset,
int length)
|
private static int |
gIndex(int n)
|
private static int |
hash(char[] key,
int offset,
int length)
|
static CToken |
lookup(char[] data,
int offset,
int length)
|
| Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
tokens
private static final CToken[] tokens
INSIDE_ANNOTATION
public static final int INSIDE_ANNOTATION
QUANTIFIER
public static final int QUANTIFIER
IGNORE_JML_ID_AFTER
public static final int IGNORE_JML_ID_AFTER
MAX_GRAPH_NODE_VAL
private static final int MAX_GRAPH_NODE_VAL
MIN_CHAR_VAL
private static final int MIN_CHAR_VAL
MAX_CHAR_VAL
private static final int MAX_CHAR_VAL
MIN_WORD_LENG
private static final int MIN_WORD_LENG
MAX_WORD_LENG
private static final int MAX_WORD_LENG
TOTAL_KEYWORDS
private static final int TOTAL_KEYWORDS
keywords
private static final char[][] keywords
T1
private static final int[][] T1
T2
private static final int[][] T2
MAX_NODE_NUM
private static final int MAX_NODE_NUM
JmlIDKeywords
JmlIDKeywords()
lookup
public static CToken lookup(char[] data,
int offset,
int length)
gIndex
private static final int gIndex(int n)
equals
private static final boolean equals(char[] key,
int offset,
int length,
char[] word)
hash
private static final int hash(char[] key,
int offset,
int length)
find
private static final int find(char[] key,
int offset,
int length)
JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.