001    /* Copyright 2000, 2001, Compaq Computer Corporation */
002    
003    package escjava.ast;
004    
005    import javafe.ast.Identifier;
006    import javafe.util.Assert;
007    
008    import escjava.prover.Atom;
009    
010    public class TagConstants extends GeneratedTags 
011            //javafe.tc.TagConstants
012        //implements GeneratedTags
013    {
014        //// Tags for new binary operators
015        public static final int IMPLIES = escjava.ast.GeneratedTags.LAST_TAG + 1;
016        public static final int EXPLIES = IMPLIES + 1;
017        public static final int IFF = EXPLIES + 1;  // equivalence (equality)
018        public static final int NIFF = IFF + 1;     // discrepance (xor)
019        public static final int SUBTYPE = NIFF + 1;
020        public static final int DOTDOT = SUBTYPE + 1;
021    
022        //// Tags for pragma punctuation
023        public static final int LEFTARROW = DOTDOT + 1; // <-
024        public static final int RIGHTARROW = LEFTARROW + 1; // ->
025        public static final int OPENPRAGMA = RIGHTARROW + 1; // {|
026        public static final int CLOSEPRAGMA = OPENPRAGMA + 1; // |}
027    
028        //// Tags for new literal expressions
029        public static final int SYMBOLLIT = CLOSEPRAGMA + 1;
030    
031        //// Tags for new primitive types
032        public static final int ANY = SYMBOLLIT + 1;
033        public static final int TYPECODE = ANY + 1;
034        public static final int BIGINTTYPE = TYPECODE + 1;
035        public static final int REALTYPE = BIGINTTYPE + 1;
036        public static final int LOCKSET = REALTYPE + 1;
037        public static final int OBJECTSET = LOCKSET + 1;
038        
039        //// Tags for guarded commands
040        public static final int ASSERTCMD = OBJECTSET + 1;
041        public static final int ASSUMECMD = ASSERTCMD + 1;
042        public static final int CHOOSECMD = ASSUMECMD + 1;
043        public static final int RAISECMD = CHOOSECMD + 1;
044        public static final int SKIPCMD = RAISECMD + 1;
045        public static final int TRYCMD = SKIPCMD + 1;
046    
047        //// Tags for special tokens
048        public static final int INFORMALPRED_TOKEN = TRYCMD + 1;
049    
050        //// Tags for ESC/Java checks
051        public static final int FIRSTESCCHECKTAG = INFORMALPRED_TOKEN + 1;
052        public static final int CHKARITHMETIC = FIRSTESCCHECKTAG;
053        public static final int CHKARRAYSTORE = CHKARITHMETIC + 1;
054        public static final int CHKASSERT = CHKARRAYSTORE + 1;
055        public static final int CHKCLASSCAST = CHKASSERT + 1;
056        public static final int CHKCODEREACHABILITY = CHKCLASSCAST + 1;
057        public static final int CHKCONSISTENT = CHKCODEREACHABILITY + 1;
058        public static final int CHKCONSTRAINT = CHKCONSISTENT + 1;
059        public static final int CHKCONSTRUCTORLEAK = CHKCONSTRAINT + 1;
060        public static final int CHKDECREASES_BOUND = CHKCONSTRUCTORLEAK + 1;
061        public static final int CHKDECREASES_DECR = CHKDECREASES_BOUND + 1;
062        public static final int CHKDEFINEDNESS = CHKDECREASES_DECR + 1;
063        public static final int CHKINDEXNEGATIVE = CHKDEFINEDNESS + 1;
064        public static final int CHKINDEXTOOBIG = CHKINDEXNEGATIVE + 1;
065        public static final int CHKINITIALIZATION = CHKINDEXTOOBIG + 1;
066        public static final int CHKINITIALIZERLEAK = CHKINITIALIZATION + 1;
067        public static final int CHKINITIALLY = CHKINITIALIZERLEAK + 1;
068        public static final int CHKLOCKINGORDER = CHKINITIALLY + 1;
069        public static final int CHKLOOPINVARIANT = CHKLOCKINGORDER + 1;
070        public static final int CHKLOOPOBJECTINVARIANT = CHKLOOPINVARIANT + 1;
071        public static final int CHKMODIFIESEXTENSION = CHKLOOPOBJECTINVARIANT + 1;
072        public static final int CHKMODIFIES = CHKMODIFIESEXTENSION + 1;
073        public static final int CHKNEGATIVEARRAYSIZE = CHKMODIFIES + 1;
074        public static final int CHKNONNULL = CHKNEGATIVEARRAYSIZE + 1;
075        public static final int CHKNONNULLINIT = CHKNONNULL + 1;
076        public static final int CHKNONNULLRESULT = CHKNONNULLINIT + 1;
077        public static final int CHKNULLPOINTER = CHKNONNULLRESULT + 1;
078        public static final int CHKOBJECTINVARIANT = CHKNULLPOINTER + 1;
079        public static final int CHKOWNERNULL = CHKOBJECTINVARIANT + 1;
080        public static final int CHKPOSTCONDITION = CHKOWNERNULL + 1;
081        public static final int CHKPRECONDITION = CHKPOSTCONDITION + 1;
082        public static final int CHKSHARING = CHKPRECONDITION + 1;
083        public static final int CHKSHARINGALLNULL = CHKSHARING + 1;
084        public static final int CHKUNENFORCEBLEOBJECTINVARIANT = CHKSHARINGALLNULL + 1;
085        public static final int CHKUNEXPECTEDEXCEPTION = CHKUNENFORCEBLEOBJECTINVARIANT + 1;
086        public static final int CHKUNEXPECTEDEXCEPTION2 = CHKUNEXPECTEDEXCEPTION + 1;
087        public static final int CHKWRITABLEDEFERRED = CHKUNEXPECTEDEXCEPTION2 + 1;
088        public static final int CHKWRITABLE = CHKWRITABLEDEFERRED + 1;
089        public static final int CHKQUIET = CHKWRITABLE + 1;
090        public static final int CHKASSUME = CHKQUIET + 1;
091        public static final int CHKADDINFO = CHKASSUME + 1;
092        public static final int CHKFREE = CHKADDINFO + 1;
093        public static final int LASTESCCHECKTAG = CHKFREE;
094    
095        //// Tags for Nary function symbols that are _not_ ESCJ keywords
096        //
097        // These need to be added both below and in escfunctions in this file,
098        // as well as as switch labels in escjava.ast.EscPrettyPrint and
099        // escjava.translate.VcToString.
100        //
101        public static final int FIRSTFUNCTIONTAG = LASTESCCHECKTAG + 1;
102        public static final int ALLOCLT = FIRSTFUNCTIONTAG;
103        public static final int ALLOCLE = ALLOCLT+1;
104        public static final int ANYEQ = ALLOCLE+1;
105        public static final int ANYNE = ANYEQ+1;
106        public static final int ARRAYLENGTH = ANYNE+1;
107        public static final int ARRAYFRESH = ARRAYLENGTH + 1;
108        public static final int ARRAYMAKE = ARRAYFRESH + 1;
109        public static final int ARRAYSHAPEMORE = ARRAYMAKE + 1;
110        public static final int ARRAYSHAPEONE = ARRAYSHAPEMORE + 1;
111        public static final int ASELEMS = ARRAYSHAPEONE + 1;
112        public static final int ASFIELD = ASELEMS + 1;
113        public static final int ASLOCKSET = ASFIELD + 1;
114        public static final int BOOLAND = ASLOCKSET + 1;
115        public static final int BOOLANDX = BOOLAND + 1;
116        public static final int BOOLEQ = BOOLANDX + 1;
117        public static final int BOOLIMPLIES = BOOLEQ + 1;
118        public static final int BOOLNE = BOOLIMPLIES + 1;
119        public static final int BOOLNOT = BOOLNE + 1;
120        public static final int BOOLOR = BOOLNOT + 1;
121        public static final int CAST = BOOLOR + 1;
122        public static final int CLASSLITERALFUNC = CAST + 1;
123        public static final int CONDITIONAL = CLASSLITERALFUNC + 1;
124        public static final int ECLOSEDTIME = CONDITIONAL + 1;
125        // ELEMSNONNULL -- an ESC keyword
126        // ELEMTYPE -- an ESC keyword
127        public static final int FCLOSEDTIME = ECLOSEDTIME + 1;
128        public static final int FLOATINGADD = FCLOSEDTIME + 1;
129        public static final int FLOATINGDIV = FLOATINGADD + 1;
130        public static final int FLOATINGEQ = FLOATINGDIV + 1;
131        public static final int FLOATINGGE = FLOATINGEQ + 1;
132        public static final int FLOATINGGT = FLOATINGGE + 1;
133        public static final int FLOATINGLE = FLOATINGGT + 1;
134        public static final int FLOATINGLT = FLOATINGLE + 1;
135        public static final int FLOATINGMOD = FLOATINGLT + 1;
136        public static final int FLOATINGMUL = FLOATINGMOD + 1;
137        public static final int FLOATINGNE = FLOATINGMUL + 1;
138        public static final int FLOATINGNEG = FLOATINGNE + 1;
139        public static final int FLOATINGSUB = FLOATINGNEG + 1;
140        public static final int INTEGRALADD = FLOATINGSUB + 1;
141        public static final int INTEGRALAND = INTEGRALADD + 1;
142        public static final int INTEGRALDIV = INTEGRALAND + 1;
143        public static final int INTEGRALEQ = INTEGRALDIV + 1;
144        public static final int INTEGRALGE = INTEGRALEQ + 1;
145        public static final int INTEGRALGT = INTEGRALGE + 1;
146        public static final int INTEGRALLE = INTEGRALGT + 1;
147        public static final int INTEGRALLT = INTEGRALLE + 1;
148        public static final int INTEGRALMOD = INTEGRALLT + 1;
149        public static final int INTEGRALMUL = INTEGRALMOD + 1;
150        public static final int INTEGRALNE = INTEGRALMUL + 1;
151        public static final int INTEGRALNEG = INTEGRALNE + 1;
152        public static final int INTEGRALNOT = INTEGRALNEG + 1;
153        public static final int INTEGRALOR = INTEGRALNOT + 1;
154        public static final int INTSHIFTL = INTEGRALOR + 1;
155        public static final int LONGSHIFTL = INTSHIFTL + 1;
156        public static final int INTSHIFTR = LONGSHIFTL + 1;
157        public static final int LONGSHIFTR = INTSHIFTR + 1;
158        public static final int INTSHIFTRU = LONGSHIFTR + 1;
159        public static final int LONGSHIFTRU = INTSHIFTRU + 1;
160        public static final int INTEGRALSUB = LONGSHIFTRU + 1;
161        public static final int INTEGRALXOR = INTEGRALSUB + 1;
162        public static final int INTERN = INTEGRALXOR + 1;
163        public static final int INTERNED = INTERN + 1;
164        public static final int IS = INTERNED + 1;
165        public static final int ISALLOCATED = IS + 1;
166        public static final int ISNEWARRAY = ISALLOCATED + 1;
167        // MAX -- an ESC keyword
168        public static final int LOCKLE = ISNEWARRAY + 1;
169        public static final int LOCKLT = LOCKLE + 1;
170        public static final int METHODCALL = LOCKLT + 1;
171        public static final int REFEQ = METHODCALL + 1;
172        public static final int REFNE = REFEQ + 1;
173        public static final int SELECT = REFNE + 1;
174        public static final int STORE = SELECT + 1;
175        public static final int STRINGCAT = STORE + 1;
176        public static final int STRINGCATP = STRINGCAT + 1;
177        public static final int TYPEEQ = STRINGCATP + 1; 
178        public static final int TYPENE = TYPEEQ + 1; 
179        public static final int TYPELE = TYPENE + 1; // a.k.a. "<:"
180        // TYPEOF -- an ESC keyword
181        public static final int UNSET = TYPELE + 1;
182        public static final int VALLOCTIME = UNSET + 1;
183        public static final int LASTFUNCTIONTAG = VALLOCTIME;
184    
185        // Constants used in deciding how to translate CHKs
186        public static final int CHK_AS_ASSUME = LASTFUNCTIONTAG + 1;
187        public static final int CHK_AS_ASSERT = CHK_AS_ASSUME + 1;
188        public static final int CHK_AS_SKIP = CHK_AS_ASSERT + 1;
189    
190    // FIXME - these should be merged into one order so they are easy to find
191    // Also keywords are looked up by a linear search - that could be improved
192    // upon greatly
193        //// JML keywords
194        public static final int FIRSTJMLKEYWORDTAG = CHK_AS_SKIP + 1;
195    
196        public static final int ASSUME = FIRSTJMLKEYWORDTAG;
197        public static final int AXIOM = ASSUME + 1;
198        public static final int CODE_CONTRACT = AXIOM + 1;
199        public static final int DECREASES = CODE_CONTRACT + 1;
200        public static final int DTTFSA = DECREASES + 1;
201        public static final int ENSURES = DTTFSA + 1;
202        public static final int ELEMSNONNULL = ENSURES + 1; // Function
203        public static final int ELEMTYPE = ELEMSNONNULL + 1; // Function
204        public static final int EXISTS = ELEMTYPE + 1;
205        public static final int EXSURES = EXISTS + 1;
206        public static final int FRESH = EXSURES + 1; // Non-GCE function
207        public static final int FORALL = FRESH + 1;
208        public static final int FUNCTION = FORALL + 1;
209        public static final int GHOST = FUNCTION + 1;
210        public static final int HELPER = GHOST + 1;
211        public static final int IMMUTABLE = HELPER + 1;
212        public static final int IN = IMMUTABLE + 1;
213        public static final int IN_REDUNDANTLY = IN + 1;
214        public static final int INTO = IN_REDUNDANTLY + 1;
215        public static final int INVARIANT = INTO + 1;
216        public static final int LBLPOS = INVARIANT + 1;
217        public static final int LBLNEG = LBLPOS + 1;
218        public static final int LOOP_INVARIANT = LBLNEG + 1;
219        public static final int LOOP_PREDICATE = LOOP_INVARIANT + 1;
220        public static final int LS = LOOP_PREDICATE + 1;
221        public static final int MAPS = LS + 1; 
222        public static final int MAPS_REDUNDANTLY = MAPS + 1; 
223        public static final int MAX = MAPS_REDUNDANTLY + 1; // Function
224        public static final int MODIFIES = MAX + 1;
225        public static final int MONITORED = MODIFIES + 1;
226        public static final int MONITORED_BY = MONITORED + 1;
227        public static final int MONITORS_FOR = MONITORED_BY + 1;
228        public static final int NON_NULL = MONITORS_FOR + 1;
229        public static final int NOWARN = NON_NULL + 1;
230        public static final int PRE = NOWARN + 1;
231        public static final int READABLE = PRE + 1;
232        public static final int READABLE_IF = READABLE + 1;
233        public static final int RES = READABLE_IF + 1;
234        public static final int REQUIRES = RES + 1;
235        public static final int SET = REQUIRES + 1;
236        public static final int SPEC_PUBLIC = SET + 1;
237        public static final int STILL_DEFERRED = SPEC_PUBLIC + 1;
238        public static final int TYPE = STILL_DEFERRED + 1;  // "type"
239        public static final int TYPETYPE = TYPE + 1;          // "TYPE"; name for TYPECODE
240        public static final int TYPEOF = TYPETYPE + 1; // Function
241        public static final int UNINITIALIZED = TYPEOF + 1;
242        public static final int UNREACHABLE = UNINITIALIZED + 1;
243        public static final int WRITABLE_DEFERRED = UNREACHABLE + 1;
244        public static final int WRITABLE_IF = WRITABLE_DEFERRED+ 1;
245        public static final int WRITABLE = WRITABLE_IF + 1;
246        public static final int SKOLEM_CONSTANT = WRITABLE + 1;
247    
248        public static final int BIGINT = SKOLEM_CONSTANT + 1;
249        public static final int WACK_DURATION = BIGINT + 1;
250        // \elemtype -- an ESC keyword
251        public static final int EVERYTHING = WACK_DURATION + 1;
252        // \exists -- an ESC keyword
253        public static final int FIELDS_OF = EVERYTHING + 1;
254        // \forall -- an ESC keyword
255        // \fresh -- an ESC keyword 
256        public static final int INVARIANT_FOR = FIELDS_OF + 1;
257        public static final int IS_INITIALIZED = INVARIANT_FOR + 1;
258        // \lblneg -- an ESC keyword
259        // \lblpos -- an ESC keyword
260        // \lockset -- an ESC keyword
261        // \max -- an ESC keyword 
262        public static final int MAXQUANT = IS_INITIALIZED + 1;
263        public static final int MIN = MAXQUANT + 1;
264        // \nonnullelements -- an ESC keyword
265        public static final int NOTHING = MIN + 1;
266        public static final int NOT_MODIFIED = NOTHING + 1;
267        public static final int NOT_SPECIFIED = NOT_MODIFIED + 1;
268        public static final int WACK_NOWARN = NOT_SPECIFIED + 1;
269        public static final int NOWARN_OP = WACK_NOWARN + 1;
270        public static final int NUM_OF = NOWARN_OP + 1;
271        // \old -- an ESC keyword
272        public static final int OTHER = NUM_OF + 1;
273        public static final int PRIVATE_DATA = OTHER + 1;
274        public static final int PRODUCT = PRIVATE_DATA + 1;
275        public static final int REACH = PRODUCT + 1;
276        public static final int REAL = REACH + 1;
277        // \result -- an ESC keyword
278        public static final int SPACE = REAL + 1;
279        public static final int SUCH_THAT = SPACE + 1;
280        public static final int SUM = SUCH_THAT + 1;
281        // \type -- an ESC keyword
282        // \typeof -- an ESC keyword
283        // \TYPE -- an ESC keyword
284        public static final int WARN = SUM + 1;
285        public static final int WARN_OP = WARN + 1;
286        public static final int WACK_WORKING_SPACE = WARN_OP + 1;
287    
288        public static final int ABRUPT_BEHAVIOR = WACK_WORKING_SPACE + 1;
289        public static final int ACCESSIBLE_REDUNDANTLY = ABRUPT_BEHAVIOR + 1;
290        public static final int ACCESSIBLE = ACCESSIBLE_REDUNDANTLY + 1;
291        public static final int ALSO = ACCESSIBLE + 1;
292        public static final int ALSO_REFINE = ALSO + 1; // Internal use only
293        public static final int ASSERT_REDUNDANTLY = ALSO_REFINE + 1;
294        public static final int ASSIGNABLE_REDUNDANTLY = ASSERT_REDUNDANTLY + 1;
295        public static final int ASSIGNABLE = ASSIGNABLE_REDUNDANTLY + 1;
296        public static final int ASSUME_REDUNDANTLY = ASSIGNABLE + 1;
297        // assume -- an ESC keyword
298        // axiom -- an ESC keyword
299        public static final int BEHAVIOR = ASSUME_REDUNDANTLY + 1;
300        public static final int BREAKS_REDUNDANTLY = BEHAVIOR + 1;
301        public static final int BREAKS = BREAKS_REDUNDANTLY + 1;
302        public static final int CALLABLE_REDUNDANTLY = BREAKS + 1;
303        public static final int CALLABLE = CALLABLE_REDUNDANTLY + 1;
304        public static final int CHOOSE_IF = CALLABLE + 1;
305        public static final int CHOOSE = CHOOSE_IF + 1;
306        public static final int CONSTRAINT_REDUNDANTLY = CHOOSE + 1;
307        public static final int CONSTRAINT = CONSTRAINT_REDUNDANTLY + 1;
308        public static final int CONSTRUCTOR = CONSTRAINT + 1;
309        public static final int CONTINUES_REDUNDANTLY = CONSTRUCTOR + 1;
310        public static final int CONTINUES = CONTINUES_REDUNDANTLY + 1; // @review
311        public static final int DECREASES_REDUNDANTLY = CONTINUES + 1;
312        // decreases -- an ESC keyword
313        public static final int DECREASING_REDUNDANTLY = DECREASES_REDUNDANTLY + 1;
314        public static final int DECREASING = DECREASING_REDUNDANTLY + 1;
315        public static final int DEPENDS_REDUNDANTLY = DECREASING + 1;
316        public static final int DEPENDS = DEPENDS_REDUNDANTLY + 1;
317        public static final int DIVERGES_REDUNDANTLY = DEPENDS + 1;
318        public static final int DIVERGES = DIVERGES_REDUNDANTLY + 1;
319        public static final int DURATION_REDUNDANTLY = DIVERGES + 1;
320        public static final int DURATION = DURATION_REDUNDANTLY + 1;
321        public static final int END = DURATION + 1; // Internal use only
322        public static final int ENSURES_REDUNDANTLY = END + 1;
323        // ensures -- an ESC keyword
324        public static final int EXAMPLE = ENSURES_REDUNDANTLY + 1;
325        public static final int EXCEPTIONAL_BEHAVIOR = EXAMPLE + 1;
326        public static final int EXCEPTIONAL_EXAMPLE = EXCEPTIONAL_BEHAVIOR + 1;
327        public static final int EXSURES_REDUNDANTLY = EXCEPTIONAL_EXAMPLE + 1;
328        public static final int FIELDKW = EXSURES_REDUNDANTLY + 1;
329        // exsures -- an ESC keyword
330        public static final int NO_WACK_FORALL = FIELDKW + 1;
331        public static final int FOR_EXAMPLE = NO_WACK_FORALL + 1;
332        // ghost -- an ESC keyword
333        public static final int IMPLIES_THAT = FOR_EXAMPLE + 1;
334        // helper -- an ESC keyword
335        public static final int HENCE_BY_REDUNDANTLY = IMPLIES_THAT + 1;
336        public static final int HENCE_BY = HENCE_BY_REDUNDANTLY + 1;
337        public static final int INITIALIZER = HENCE_BY + 1;
338        public static final int INITIALLY = INITIALIZER + 1;
339        public static final int INSTANCE = INITIALLY + 1;
340        public static final int INVARIANT_REDUNDANTLY = INSTANCE + 1;
341        // invariant -- an ESC keyword
342        public static final int LOOP_INVARIANT_REDUNDANTLY = INVARIANT_REDUNDANTLY + 1;
343        // loop_invariant -- an ESC keyword
344        public static final int MAINTAINING_REDUNDANTLY = LOOP_INVARIANT_REDUNDANTLY + 1;
345        public static final int MAINTAINING = MAINTAINING_REDUNDANTLY + 1;
346        public static final int MEASURED_BY_REDUNDANTLY = MAINTAINING + 1;
347        public static final int MEASURED_BY = MEASURED_BY_REDUNDANTLY + 1;
348        public static final int METHOD = MEASURED_BY + 1;
349        public static final int MODEL = METHOD + 1;
350        public static final int MODEL_PROGRAM = MODEL + 1;
351        public static final int MODIFIABLE_REDUNDANTLY = MODEL_PROGRAM + 1;
352        public static final int MODIFIABLE = MODIFIABLE_REDUNDANTLY + 1;
353        public static final int MODIFIES_REDUNDANTLY = MODIFIABLE + 1;
354        // modifies -- an ESC keyword
355        // monitored_by -- an ESC keyword
356        // monitored -- an ESC keyword
357        public static final int NESTEDMODIFIERPRAGMA = MODIFIES_REDUNDANTLY + 1;
358        // non_null -- an ESC keyword
359        public static final int NORMAL_BEHAVIOR = NESTEDMODIFIERPRAGMA + 1;
360        public static final int NORMAL_EXAMPLE = NORMAL_BEHAVIOR + 1;
361        // nowarn -- an ESC keyword
362        public static final int OLD = NORMAL_EXAMPLE + 1;
363        public static final int MODELPROGRAM_OR = OLD + 1;
364        public static final int PARSEDSPECS = MODELPROGRAM_OR + 1;
365        public static final int POSTCONDITION_REDUNDANTLY = PARSEDSPECS + 1;
366        public static final int POSTCONDITION = POSTCONDITION_REDUNDANTLY + 1;
367        public static final int PRECONDITION_REDUNDANTLY = POSTCONDITION + 1;
368        public static final int PRECONDITION = PRECONDITION_REDUNDANTLY + 1;
369        public static final int PURE = PRECONDITION + 1;
370        // readable_if -- an ESC keyword
371        public static final int REFINE = PURE + 1;
372        public static final int REPRESENTS_REDUNDANTLY = REFINE + 1;
373        public static final int REPRESENTS = REPRESENTS_REDUNDANTLY + 1;
374        public static final int REQUIRES_REDUNDANTLY = REPRESENTS + 1;
375        // requires -- an ESC keyword
376        public static final int RETURNS_REDUNDANTLY = REQUIRES_REDUNDANTLY + 1;
377        public static final int RETURNS = RETURNS_REDUNDANTLY + 1;
378        // set -- an ESC keyword
379        public static final int SIGNALS_REDUNDANTLY = RETURNS + 1;
380        public static final int SIGNALS = SIGNALS_REDUNDANTLY + 1;
381        public static final int SIGNALS_ONLY = SIGNALS + 1;
382        public static final int SPEC_PROTECTED = SIGNALS_ONLY + 1;
383        // spec_public -- an ESC keyword
384        public static final int STATIC_INITIALIZER = SPEC_PROTECTED + 1;
385        public static final int SUBCLASSING_CONTRACT = STATIC_INITIALIZER + 1;
386        // uninitialized -- an ESC keyword
387        // unreachable -- an ESC keyword
388        public static final int WEAKLY = SUBCLASSING_CONTRACT + 1;
389        public static final int WHEN_REDUNDANTLY = WEAKLY + 1;
390        public static final int WHEN = WHEN_REDUNDANTLY + 1;
391        public static final int WORKING_SPACE_REDUNDANTLY = WHEN + 1;
392        public static final int WORKING_SPACE = WORKING_SPACE_REDUNDANTLY + 1;
393    
394        public static final int LASTJMLKEYWORDTAG = WORKING_SPACE;
395    
396        //// Tags for ESCJ keywords
397        // These are keywords that are not in JML (either obsolete or
398        // extensions), or are tokens for internal use only
399        // Be sure to keep the esckeywords[] array in synch
400        public static final int FIRSTESCKEYWORDTAG = LASTJMLKEYWORDTAG + 1;
401        public static final int ALSO_ENSURES = FIRSTESCKEYWORDTAG;
402        public static final int ALSO_EXSURES = ALSO_ENSURES + 1;
403        public static final int ALSO_MODIFIES = ALSO_EXSURES + 1;
404        public static final int ALSO_REQUIRES = ALSO_MODIFIES + 1;
405    
406        // Include the Universe type annotation keywords (cjbooms)
407        public static final int PEER = ALSO_REQUIRES + 1;
408        public static final int READONLY = PEER + 1;
409        public static final int REP = READONLY + 1;
410    
411        // Chalin-Kiniry experimental keywords for nullness, purity, and whatnot
412        public static final int MAY_BE_NULL = REP + 1;
413        public static final int NULL_REF_BY_DEFAULT = MAY_BE_NULL + 1;
414        public static final int NON_NULL_REF_BY_DEFAULT = NULL_REF_BY_DEFAULT + 1;
415        public static final int OBS_PURE = NON_NULL_REF_BY_DEFAULT + 1;
416    
417        // Chalin's spec and code modifiers for different math semantics
418        public static final int WACK_JAVA_MATH = OBS_PURE + 1;
419        public static final int WACK_SAFE_MATH = WACK_JAVA_MATH + 1;
420        public static final int WACK_BIGINT_MATH = WACK_SAFE_MATH + 1;
421        public static final int CODE_JAVA_MATH = WACK_BIGINT_MATH + 1;
422        public static final int CODE_SAFE_MATH = CODE_JAVA_MATH + 1;
423        public static final int CODE_BIGINT_MATH = CODE_SAFE_MATH + 1;
424        public static final int SPEC_JAVA_MATH = CODE_BIGINT_MATH + 1;
425        public static final int SPEC_SAFE_MATH = SPEC_JAVA_MATH + 1;
426        public static final int SPEC_BIGINT_MATH = SPEC_SAFE_MATH + 1;
427    
428        public static final int LASTESCKEYWORDTAG = SPEC_BIGINT_MATH;
429    
430        public static final int LAST_TAG = LASTESCKEYWORDTAG;
431    
432        public static final /*@non_null*/ Identifier ExsuresIdnName = 
433            Identifier.intern("Optional..Exsures..Id..Name");
434    
435        //// Helper functions
436    
437        public static /*@non_null*/ String toVcString(int tag) {
438            switch(tag) {
439                case TYPECODE:
440                    return "TYPECODE";              // displayed to user as "TYPE"
441                default:
442                    break;
443            }
444    
445            String s = toString(tag);
446            //@ assume s.length() > 0;
447            if (s.charAt(0) == '\\') {
448                s = s.substring(1);
449            }
450            if (s.equals("lockset")) {
451                s = "LS";
452            } else if (s.equals("result")) {
453                s = "RES";
454            }
455            return s;
456        }
457    
458        // Documented in parent.
459    
460        public static /*@non_null*/ String toString(int tag) {
461            switch(tag) {
462                // new literal expression (not true keyword)
463                case  SYMBOLLIT:
464                    return "*SYMBOLLIT*";
465                // guarded commands (not true keywords)
466                case ASSERTCMD:
467                    return "*ASSERTCMD*";
468                case ASSUMECMD:
469                    return "*ASSUMECMD*";
470                case CHOOSECMD:
471                    return "*CHOOSECMD*";
472                case RAISECMD:
473                    return "*RAISECMD*";
474                case SKIPCMD:
475                    return "*SKIPCMD*";
476                case TRYCMD:
477                    return "*TRYCMD*";
478                // informal predicates (not true keyword)
479                case INFORMALPRED_TOKEN:
480                    return "*INFORMAL_PREDICATE*";
481                // special symbols
482                case IMPLIES:
483                    return "==>";
484                case EXPLIES:
485                    return "<==";
486                case IFF:
487                    return "<==>";
488                case NIFF:
489                    return "<=!=>";
490                case SUBTYPE:
491                    return "<:";
492                case DOTDOT:
493                    return "..";
494                case LEFTARROW:
495                    return "<-";
496                case RIGHTARROW:
497                    return "->";
498                case OPENPRAGMA:
499                    return "{|";
500                case CLOSEPRAGMA:
501                    return "|}";
502                case ANY:
503                    return "ANY";
504                case TYPECODE:
505                    //return "TYPECODE";            // displayed to user as "TYPE"
506                    return "TYPE";
507                case LOCKSET:
508                    return "LOCKSET";
509                case OBJECTSET:
510                    return "OBJECTSET";
511                case CHK_AS_ASSUME:
512                    return "CHK_AS_ASSUME";
513                case CHK_AS_ASSERT:
514                    return "CHK_AS_ASSERT";
515                case CHK_AS_SKIP:
516                    return "CHK_AS_SKIP";
517                default:
518                    if (FIRSTESCKEYWORDTAG <= tag && tag <= LASTESCKEYWORDTAG)
519                        return esckeywords[tag - FIRSTESCKEYWORDTAG].toString();
520                    else if (FIRSTESCCHECKTAG <= tag && tag <= LASTESCCHECKTAG)
521                        return escchecks[tag - FIRSTESCCHECKTAG];
522                    else if (FIRSTFUNCTIONTAG <= tag && tag <= LASTFUNCTIONTAG)
523                        return escfunctions[tag - FIRSTFUNCTIONTAG];
524                    else if (FIRSTJMLKEYWORDTAG <= tag && tag <= LASTJMLKEYWORDTAG)
525                        return jmlkeywords[tag - FIRSTJMLKEYWORDTAG].toString();
526                    else if (tag == TagConstants.MODIFIESGROUPPRAGMA)
527                        return "modifies";
528                    else if (tag <= GeneratedTags.LAST_TAG)
529                        return GeneratedTags.toString(tag);
530                    else {
531                        return "Unknown ESC tag <" + tag
532                            + " (+" + (tag - javafe.tc.TagConstants.LAST_TAG) + ") >";
533                    }
534            }
535        }
536    
537        /**
538         * @param keyword the keyword to lookup.
539         * @return the index of the {@link TagConstants} attribute
540         * corresponding to the keyword encoded as an {@link Identifier}
541         * in the parameter 'keyword'. A {@link #NULL} is returned if
542         * the identifier in question is not an ESC/Java or JML keyword
543         * known to {@link TagConstants}.
544         */
545        public static int fromIdentifier(Identifier keyword) {
546            for(int i = 0; i < jmlkeywords.length; i++)
547                if (keyword == jmlkeywords[i]) return i + FIRSTJMLKEYWORDTAG;
548            for(int i = 0; i < esckeywords.length; i++)
549                if (keyword == esckeywords[i]) return i + FIRSTESCKEYWORDTAG;
550            return NULL;
551        }
552    
553        public static boolean isKeywordTag(int tag) {
554            return (FIRSTJMLKEYWORDTAG <= tag && tag <= LASTJMLKEYWORDTAG)
555              || (FIRSTESCKEYWORDTAG <= tag && tag <= LASTESCKEYWORDTAG);
556        }
557    
558        public static int checkFromString(/*@non_null*/ String s) {
559            for (int i = FIRSTESCCHECKTAG; i <= LASTESCCHECKTAG; i++) {
560                if (s.equals(escchecks[i - FIRSTESCCHECKTAG]))
561                    return i;
562            }
563            //@ unreachable;
564            Assert.fail("unrecognized check string: \"" + s + "\"");
565            return -1;
566        }
567    
568        /**
569         * @return a "redundant-fied" version of the passed tag if it can
570         * be made redundant; otherwise, return the parameter unchanged.
571         */
572        public static int makeRedundant(int tag) {
573            int Result = tag;
574            switch (tag) {
575                case TagConstants.REQUIRES:
576                    Result = TagConstants.REQUIRES_REDUNDANTLY; break;
577                case TagConstants.ENSURES:
578                    Result = TagConstants.ENSURES_REDUNDANTLY; break;
579                case TagConstants.PRECONDITION:
580                    Result = TagConstants.PRECONDITION_REDUNDANTLY; break;
581                case TagConstants.DIVERGES:
582                    Result = TagConstants.DIVERGES_REDUNDANTLY; break;
583                case TagConstants.WHEN:
584                    Result = TagConstants.WHEN_REDUNDANTLY; break;
585                case TagConstants.POSTCONDITION:
586                    Result = TagConstants.POSTCONDITION_REDUNDANTLY; break;
587                case TagConstants.EXSURES:
588                    Result = TagConstants.EXSURES_REDUNDANTLY; break;
589                case TagConstants.SIGNALS:
590                    Result = TagConstants.SIGNALS_REDUNDANTLY; break;
591                case TagConstants.MODIFIABLE:
592                    Result = TagConstants.MODIFIABLE_REDUNDANTLY; break;
593                case TagConstants.ASSIGNABLE:
594                    Result = TagConstants.ASSIGNABLE_REDUNDANTLY; break;
595                case TagConstants.MODIFIES:
596                    Result = TagConstants.MODIFIES_REDUNDANTLY; break;
597                case TagConstants.MEASURED_BY:
598                    Result = TagConstants.MEASURED_BY_REDUNDANTLY; break;
599                case TagConstants.ASSERT:
600                    Result = TagConstants.ASSERT_REDUNDANTLY; break;
601                case TagConstants.ASSUME:
602                    Result = TagConstants.ASSUME_REDUNDANTLY; break;
603                case TagConstants.LOOP_INVARIANT:
604                    Result = TagConstants.LOOP_INVARIANT_REDUNDANTLY; break;
605                case TagConstants.MAINTAINING:
606                    Result = TagConstants.MAINTAINING_REDUNDANTLY; break;
607                case TagConstants.DECREASES:
608                    Result = TagConstants.DECREASES_REDUNDANTLY; break;
609                case TagConstants.INVARIANT:
610                    Result = TagConstants.INVARIANT_REDUNDANTLY; break;
611                case TagConstants.REPRESENTS:
612                    Result = TagConstants.REPRESENTS_REDUNDANTLY; break;
613                case TagConstants.CONSTRAINT:
614                    Result = TagConstants.CONSTRAINT_REDUNDANTLY; break;
615                case TagConstants.DECREASING:
616                    Result = TagConstants.DECREASING_REDUNDANTLY; break;
617                case TagConstants.DURATION:
618                    Result = TagConstants.DURATION_REDUNDANTLY; break;
619                case TagConstants.WORKING_SPACE:
620                    Result = TagConstants.WORKING_SPACE_REDUNDANTLY; break;
621                case TagConstants.IN:
622                    Result = TagConstants.IN_REDUNDANTLY; break;
623                case TagConstants.MAPS:
624                    Result = TagConstants.MAPS_REDUNDANTLY; break;
625                case TagConstants.HENCE_BY:
626                    Result = TagConstants.HENCE_BY_REDUNDANTLY; break;
627            }
628            return Result;
629        }
630        
631        /**
632         * @return an "unredundant-fied" version of the passed tag if it
633         * is redundant; otherwise, return the parameter unchanged.
634         */
635        public static int unRedundant(int tag) {
636            int Result = tag;
637            switch (tag) {
638                      case TagConstants.REQUIRES_REDUNDANTLY:
639                    Result = TagConstants.REQUIRES; break;
640                case TagConstants.ENSURES_REDUNDANTLY:
641                    Result = TagConstants.ENSURES; break;
642                case TagConstants.PRECONDITION_REDUNDANTLY:
643                    Result = TagConstants.PRECONDITION; break;
644                case TagConstants.DIVERGES_REDUNDANTLY:
645                    Result = TagConstants.DIVERGES; break;
646                case TagConstants.WHEN_REDUNDANTLY:
647                    Result = TagConstants.WHEN; break;
648                case TagConstants.POSTCONDITION_REDUNDANTLY:
649                    Result = TagConstants.POSTCONDITION; break;
650                case TagConstants.EXSURES_REDUNDANTLY:
651                    Result = TagConstants.EXSURES; break;
652                case TagConstants.SIGNALS_REDUNDANTLY:
653                    Result = TagConstants.SIGNALS; break;
654                case TagConstants.MODIFIABLE_REDUNDANTLY:
655                    Result = TagConstants.MODIFIABLE; break;
656                case TagConstants.ASSIGNABLE_REDUNDANTLY:
657                    Result = TagConstants.ASSIGNABLE; break;
658                case TagConstants.MODIFIES_REDUNDANTLY:
659                    Result = TagConstants.MODIFIES; break;
660                case TagConstants.MEASURED_BY_REDUNDANTLY:
661                    Result = TagConstants.MEASURED_BY; break;
662                case TagConstants.ASSERT_REDUNDANTLY:
663                    Result = TagConstants.ASSERT; break;
664                case TagConstants.ASSUME_REDUNDANTLY:
665                    Result = TagConstants.ASSUME; break;
666                case TagConstants.LOOP_INVARIANT_REDUNDANTLY:
667                    Result = TagConstants.LOOP_INVARIANT; break;
668                case TagConstants.MAINTAINING_REDUNDANTLY:
669                    Result = TagConstants.MAINTAINING; break;
670                case TagConstants.DECREASES_REDUNDANTLY:
671                    Result = TagConstants.DECREASES; break;
672                case TagConstants.INVARIANT_REDUNDANTLY:
673                    Result = TagConstants.INVARIANT; break;
674                case TagConstants.REPRESENTS_REDUNDANTLY:
675                    Result = TagConstants.REPRESENTS; break;
676                case TagConstants.CONSTRAINT_REDUNDANTLY:
677                    Result = TagConstants.CONSTRAINT; break;
678                case TagConstants.DECREASING_REDUNDANTLY:
679                    Result = TagConstants.DECREASING; break;
680                case TagConstants.DURATION_REDUNDANTLY:
681                    Result = TagConstants.DURATION; break;
682                case TagConstants.WORKING_SPACE_REDUNDANTLY:
683                    Result = TagConstants.WORKING_SPACE; break;
684                case TagConstants.IN_REDUNDANTLY:
685                    Result = TagConstants.IN; break;
686                case TagConstants.MAPS_REDUNDANTLY:
687                    Result = TagConstants.MAPS; break;
688                case TagConstants.HENCE_BY_REDUNDANTLY:
689                    Result = TagConstants.HENCE_BY; break;
690            }
691            return Result;
692        }
693    
694        public static boolean isRedundant(int tag) {
695          return (tag == TagConstants.REQUIRES_REDUNDANTLY
696                  || tag == TagConstants.ASSERT_REDUNDANTLY
697                  || tag == TagConstants.ASSIGNABLE_REDUNDANTLY
698                  || tag == TagConstants.ASSUME_REDUNDANTLY
699                  || tag == TagConstants.CONSTRAINT_REDUNDANTLY
700                  || tag == TagConstants.DECREASES_REDUNDANTLY
701                  || tag == TagConstants.DECREASING_REDUNDANTLY
702                  || tag == TagConstants.DIVERGES_REDUNDANTLY
703                  || tag == TagConstants.DURATION_REDUNDANTLY
704                  || tag == TagConstants.ENSURES_REDUNDANTLY
705                  || tag == TagConstants.EXSURES_REDUNDANTLY
706                  || tag == TagConstants.HENCE_BY_REDUNDANTLY
707                  || tag == TagConstants.INVARIANT_REDUNDANTLY
708                  || tag == TagConstants.IN_REDUNDANTLY
709                  || tag == TagConstants.LOOP_INVARIANT_REDUNDANTLY
710                  || tag == TagConstants.MAINTAINING_REDUNDANTLY
711                  || tag == TagConstants.MAPS_REDUNDANTLY
712                  || tag == TagConstants.MEASURED_BY_REDUNDANTLY
713                  || tag == TagConstants.MODIFIABLE_REDUNDANTLY
714                  || tag == TagConstants.MODIFIES_REDUNDANTLY
715                  || tag == TagConstants.POSTCONDITION_REDUNDANTLY
716                  || tag == TagConstants.PRECONDITION_REDUNDANTLY
717                  || tag == TagConstants.REPRESENTS_REDUNDANTLY
718                  || tag == TagConstants.SIGNALS_REDUNDANTLY
719                  || tag == TagConstants.WHEN_REDUNDANTLY
720                  || tag == TagConstants.WORKING_SPACE_REDUNDANTLY
721                  );
722        }
723    
724        public final static /*@non_null*/ String[] escchecks = {
725            "ZeroDiv",
726            "ArrayStore",
727            "Assert",
728            "Cast",
729            "Reachable",
730            "Inconsistent",
731            "Constraint",
732            "CLeak",
733            "DecreasesBound",
734            "Decreases",
735            "Unreadable",
736            "IndexNegative",
737            "IndexTooBig",
738            "Uninit",
739            "ILeak",
740            "Initially",
741            "Deadlock",
742            "LoopInv",
743            "LoopObjInv",
744            "ModExt",
745            "Modifies",
746            "NegSize",
747            "NonNull",
748            "NonNullInit",
749            "NonNullResult",
750            "Null",
751            "Invariant",
752            "OwnerNull",
753            "Post",
754            "Pre",
755            "Race",
756            "RaceAllNull",
757            "Unenforcable",
758            "Exception",
759            "SpecificationException",
760            "Deferred",
761            "Writable",
762            "vc.Quiet",  // printed in debugging output only
763            "Assume",  // internal use only
764            "AdditionalInfo", // internal use only
765            "Free"  // printed in debugging output only
766        };
767            
768        private static /*@non_null*/ String[] escfunctions = {
769            "allocLT",
770            "allocLE",
771            "anyEQ",
772            "anyNE",
773            "arrayLength",
774            "arrayFresh",
775            "arrayMake",
776            "arrayShapeMore",
777            "arrayShapeOne",
778            "asElems",
779            "asField",
780            "asLockSet",
781            "boolAnd",
782            "boolAndX",
783            "boolEq",
784            "boolImplies",
785            "boolNE",
786            "boolNot",
787            "boolOr",
788            "cast",
789            "classLiteral",
790            "termConditional",
791            "eClosedTime",
792            "fClosedTime",
793            "floatingAdd",
794            "floatingDiv",
795            "floatingEQ",
796            "floatingGE",
797            "floatingGT",
798            "floatingLE",
799            "floatingLT",
800            "floatingMod",
801            "floatingMul",
802            "floatingNE",
803            "floatingNeg",
804            "floatingSub",
805            "integralAdd",
806            "integralAnd",
807            "integralDiv",
808            "integralEQ",
809            "integralGE",
810            "integralGT",
811            "integralLE",
812            "integralLT",
813            "integralMod",
814            "integralMul",
815            "integralNE",
816            "integralNeg",
817            "integralNot",
818            "integralOr",
819            "intShiftL",
820            "longShiftL",
821            "intShiftAR",
822            "longShiftAR",
823            "intShiftUR",
824            "longShiftUR",
825            "integralSub",
826            "integralXor",
827            "|intern:|", // maps int to String for Strings interned by ESC/Java
828            "|interned:|", // maps String to boolean to say whether a String is interned, per Java semantics
829            "is",
830            "isAllocated",
831            "isNewArray",
832            "lockLE",
833            "lockLT",
834            "methodCall",
835            "refEQ",
836            "refNE",
837            "select",
838            "store",
839            "stringCat",
840            "stringCatP",
841            "typeEQ",
842            "typeNE",
843            "typeLE",
844            "unset",
845            "vAllocTime"
846        };
847    
848        static public final String STRINGCATINFIX = "java.lang.String._infixConcat_";
849                                         // Must match method name in String.spec
850    
851        private static /*@non_null*/ Identifier[] jmlkeywords = {
852            Identifier.intern("assume"),
853            Identifier.intern("axiom"),
854            Identifier.intern("code_contract"),
855            Identifier.intern("decreases"),
856            Identifier.intern("\\dttfsa"),
857            Identifier.intern("ensures"),
858            Identifier.intern("\\nonnullelements"),
859            Identifier.intern("\\elemtype"),
860            Identifier.intern("\\exists"),
861            Identifier.intern("exsures"),
862            Identifier.intern("\\fresh"),
863            Identifier.intern("\\forall"),
864            Identifier.intern("function"),
865            Identifier.intern("ghost"),
866            Identifier.intern("helper"),
867            Identifier.intern("immutable"),
868            Identifier.intern("in"),
869            Identifier.intern("in_redundantly"),
870            Identifier.intern("\\into"),
871            Identifier.intern("invariant"),
872            Identifier.intern("\\lblpos"),
873            Identifier.intern("\\lblneg"),
874            Identifier.intern("loop_invariant"),
875            Identifier.intern("loop_predicate"),
876            Identifier.intern("\\lockset"),
877            Identifier.intern("maps"),
878            Identifier.intern("maps_redundantly"),
879            Identifier.intern("\\max"),
880            Identifier.intern("modifies"),
881            Identifier.intern("monitored"),
882            Identifier.intern("monitored_by"),
883            Identifier.intern("monitors_for"),
884            Identifier.intern("non_null"),
885            Identifier.intern("nowarn"),
886            Identifier.intern("\\old"),  // TagConstants.PRE
887            Identifier.intern("readable"),
888            Identifier.intern("readable_if"),
889            Identifier.intern("\\result"),
890            Identifier.intern("requires"),
891            Identifier.intern("set"),
892            Identifier.intern("spec_public"),
893            Identifier.intern("still_deferred"),
894            Identifier.intern("\\type"),                    // TYPE
895            Identifier.intern("\\TYPE"),                    // TYPETYPE
896            Identifier.intern("\\typeof"),
897            Identifier.intern("uninitialized"),
898            Identifier.intern("unreachable"),
899            Identifier.intern("writable_deferred"),
900            Identifier.intern("writable_if"),
901            Identifier.intern("writable"),
902            Identifier.intern("skolem_constant"),
903            Identifier.intern("\\bigint"),
904            Identifier.intern("\\duration"),
905            Identifier.intern("\\everything"),
906            Identifier.intern("\\fields_of"),
907            Identifier.intern("\\invariant_for"),
908            Identifier.intern("\\is_initialized"),
909            Identifier.intern("\\max"),
910            Identifier.intern("\\min"),
911            Identifier.intern("\\nothing"),
912            Identifier.intern("\\not_modified"),
913            Identifier.intern("\\not_specified"),
914            Identifier.intern("\\nowarn"),
915            Identifier.intern("\\nowarn_op"),
916            Identifier.intern("\\num_of"),
917            Identifier.intern("\\other"),
918            Identifier.intern("\\private_data"),
919            Identifier.intern("\\product"),
920            Identifier.intern("\\reach"),
921            Identifier.intern("\\real"),
922            Identifier.intern("\\space"),
923            Identifier.intern("\\such_that"),
924            Identifier.intern("\\sum"),
925            Identifier.intern("\\warn"),
926            Identifier.intern("\\warn_op"),
927            Identifier.intern("\\working_space"),
928            Identifier.intern("abrupt_behavior"),
929            Identifier.intern("accessible_redundantly"),
930            Identifier.intern("accessible"),
931            Identifier.intern("also"),
932            Identifier.intern("---also_refine---"), // internal use only
933            Identifier.intern("assert_redundantly"),
934            Identifier.intern("assignable_redundantly"),
935            Identifier.intern("assignable"),
936            Identifier.intern("assume_redundantly"),
937            Identifier.intern("behavior"),
938            Identifier.intern("breaks_redundantly"),
939            Identifier.intern("breaks"),
940            Identifier.intern("callable_redundantly"),
941            Identifier.intern("callable"),
942            Identifier.intern("choose_if"),
943            Identifier.intern("choose"),
944            Identifier.intern("constraint_redundantly"),
945            Identifier.intern("constraint"),
946            Identifier.intern("constructor"),
947            Identifier.intern("continues_redundantly"),
948            Identifier.intern("continues"),
949            Identifier.intern("decreases_redundantly"),
950            Identifier.intern("decreasing_redundantly"),
951            Identifier.intern("decreasing"),
952            Identifier.intern("depends_redundantly"),
953            Identifier.intern("depends"),
954            Identifier.intern("diverges_redundantly"),
955            Identifier.intern("diverges"),
956            Identifier.intern("duration_redundantly"),
957            Identifier.intern("duration"),
958            Identifier.intern("---end---"), // Internal use only
959            Identifier.intern("ensures_redundantly"),
960            Identifier.intern("example"),
961            Identifier.intern("exceptional_behavior"),
962            Identifier.intern("exceptional_example"),
963            Identifier.intern("exsures_redundantly"),
964            Identifier.intern("field"),
965            Identifier.intern("forall"),
966            Identifier.intern("for_example"),
967            Identifier.intern("implies_that"),
968            Identifier.intern("hence_by_redundantly"),
969            Identifier.intern("hence_by"),
970            Identifier.intern("initializer"),
971            Identifier.intern("initially"),
972            Identifier.intern("instance"),
973            Identifier.intern("invariant_redundantly"),
974            Identifier.intern("loop_invariant_redundantly"),
975            Identifier.intern("maintaining_redundantly"),
976            Identifier.intern("maintaining"),
977            Identifier.intern("measured_by_redundantly"),
978            Identifier.intern("measured_by"),
979            Identifier.intern("method"),
980            Identifier.intern("model"),
981            Identifier.intern("model_program"),
982            Identifier.intern("modifiable_redundantly"),
983            Identifier.intern("modifiable"),
984            Identifier.intern("modifies_redundantly"),
985            Identifier.intern("--- nested specs ---"),
986            Identifier.intern("normal_behavior"),
987            Identifier.intern("normal_example"),
988            Identifier.intern("old"),
989            Identifier.intern("or"),
990            Identifier.intern("--- parsed specs ---"),
991            Identifier.intern("post_redundantly"),
992            Identifier.intern("post"),
993            Identifier.intern("pre_redundantly"),
994            Identifier.intern("pre"), // PRE not PRE (which is \old )
995            Identifier.intern("pure"),
996            Identifier.intern("refine"),
997            Identifier.intern("represents_redundantly"),
998            Identifier.intern("represents"),
999            Identifier.intern("requires_redundantly"),
1000            Identifier.intern("returns_redundantly"),
1001            Identifier.intern("returns"),
1002            Identifier.intern("signals_redundantly"),
1003            Identifier.intern("signals"),
1004            Identifier.intern("signals_only"),
1005            Identifier.intern("spec_protected"),
1006            Identifier.intern("static_initializer"),
1007            Identifier.intern("subclassing_contract"),
1008            Identifier.intern("weakly"),
1009            Identifier.intern("when_redundantly"),
1010            Identifier.intern("when"),
1011            Identifier.intern("working_space_redundantly"),
1012            Identifier.intern("working_space")
1013        };
1014    
1015        private static /*@non_null*/ Identifier[] esckeywords = {
1016            Identifier.intern("also_ensures"),
1017            Identifier.intern("also_exsures"),
1018            Identifier.intern("also_modifies"),
1019            Identifier.intern("also_requires"),
1020    
1021            // Universe type annotations (cjbooms)
1022            Identifier.intern("\\peer"),
1023            Identifier.intern("\\readonly"),
1024            Identifier.intern("\\rep"),
1025    
1026            // Chalin-Kiniry experimental keywords for nullness, purity, and whatnot
1027            Identifier.intern("may_be_null"),
1028            Identifier.intern("null_ref_by_default"),
1029            Identifier.intern("non_null_ref_by_default"),
1030            Identifier.intern("obs_pure"),
1031    
1032            // Chalin's spec and code modifiers for different math semantics
1033            Identifier.intern("\\java_math"),
1034            Identifier.intern("\\safe_math"),
1035            Identifier.intern("\\bigint_math"),
1036            Identifier.intern("code_java_math"),
1037            Identifier.intern("code_safe_math"),
1038            Identifier.intern("code_bigint_math"),
1039            Identifier.intern("spec_java_math"),
1040            Identifier.intern("spec_safe_math"),
1041            Identifier.intern("spec_bigint_math")
1042        };
1043    
1044        public static void main(/*@ non_null @*/ String[] args) {
1045            for(int i = FIRST_TAG; i <= LAST_TAG; i++ )
1046                System.out.println(i + " " + toString(i));
1047        }
1048    
1049        // This initialization code is simply a quick check that the arrays
1050        // are consistent in length.
1051    
1052        static private void comp(int i, int j, /*@non_null*/ String s) {
1053            if (i != j)
1054                    System.out.println("Mismatched length ("
1055                            + i + " vs. " + j + ") in " + s);
1056        }
1057    
1058        static {
1059            comp(esckeywords.length, LASTESCKEYWORDTAG - FIRSTESCKEYWORDTAG + 1,
1060                    "esckeywords");
1061            comp(jmlkeywords.length, LASTJMLKEYWORDTAG - FIRSTJMLKEYWORDTAG + 1,
1062                    "jmlkeywords");
1063            comp(escfunctions.length, LASTFUNCTIONTAG - FIRSTFUNCTIONTAG + 1,
1064                    "escfunctions");
1065            comp(escchecks.length, LASTESCCHECKTAG - FIRSTESCCHECKTAG + 1,
1066                    "escchecks");
1067        }
1068    }