Overview  Package  Class  Use  Tree  Deprecated  Index  Help 
 PREV   NEXT FRAMES    NO FRAMES    

Constant Field Values

Contents
jack.plugin.*

jack.plugin.Generator
public static final java.lang.String ECLIPSE_RESOURCE_KEY "jack.plugin.eclipseresource"
public static final java.lang.String PROBLEM_MARKER_TYPE "jack.plugin.jackproblem"

jack.plugin.JackJml2bConfiguration
public static final java.lang.String EVERYTHING "\\everything"
public static final int EXSURES_EXCEPTION_FALSE 0
public static final int EXSURES_EXCEPTION_TRUE 1
public static final int EXSURES_OTHER 3
public static final int EXSURES_RUNTIMEEXCEPTION_FALSE 2
public static final java.lang.String NOTHING "\\nothing"

jack.plugin.JackPlugin
public static final java.lang.String ALWAYS_COMPILE_BEFORE_EDITING "always_compile_before_editing"
public static final java.lang.String ALWAYS_COMPILE_BEFORE_PROVING "always_compile_before_proving"
public static final java.lang.String ALWAYS_SAVE_BEFORE_COMPILING "always_save_before_compiling"
public static final java.lang.String ALWAYS_SAVE_BEFORE_EDITING "always_save_before_editing"
public static final java.lang.String ALWAYS_SAVE_BEFORE_PROVING "always_save_before_proving"
public static final java.lang.String CASE_EXPLORER_VIEW_ID "jack.plugin.perspective.CaseExplorer"
public static final java.lang.String DIALOG_TITLE "Jack Plugin"
public static final java.lang.String IMAGE_NAME "classes.bin"
public static final java.lang.String JACK_GENERATE "jackGenerate"
public static final java.lang.String JACK_METRICS_VIEW_ID "jack.plugin.metricsview"
public static final java.lang.String JACK_OBVIOUS_PO "jackObviousPo"
public static final java.lang.String JACK_PERSPECTIVE_ID "jack.plugin.perspective.JackPerspective"
public static final java.lang.String JACK_PROOF_TASK_MAX_RUNNING "jackPoofTaskMaxRunning"
public static final java.lang.String JACK_PROOF_VIEW_ID "jack.plugin.proofview"
public static final java.lang.String JACK_SUBDIRECTORY "jackJpoDir"
public static final java.lang.String JACK_VIEW_ID "jack.plugin.poview"
public static final java.lang.String JACK_VIEW_SHOW "jackViewShow"
public static final java.lang.String JACK_VIEWER_FONT "jackViewerFont"
public static final java.lang.String JACK_WELLDEF_LEMMA "jackWellDefLemma"
public static final java.lang.String JML_KEYWORD_COLOR "jmlkeywordcolor"
public static final java.lang.String JMLPATH_PREFERENCE "jackJmlPath"
public static final java.lang.String LEMMA_VIEWER "jack.plugin.perspective.LemmaViewer"
public static final java.lang.String MULTI_COMMENT_JML_COLOR "multicommentjmlcolor"
public static final java.lang.String OBVIOUS_PROVER "obviousProver"
public static final java.lang.String PROVER_EXTENSION_ID "jack.plugin.Prover"
public static final java.lang.String SINGLE_COMMENT_JML_COLOR "singlecommentjmlcolor"
public static final java.lang.String SOURCE_CASE_VIEWER_ID "jack.plugin.perspective.SourceCaseViewer"

jack.plugin.edit.JavaLineStyler
public static final int EOF -1
public static final int EOL 10
public static final int KEY 2
public static final int KEY_JML 9
public static final int MAXIMUM_TOKEN 12
public static final int MULTI_COMMENT 3
public static final int MULTI_COMMENT_JML 8
public static final int NUMBER 7
public static final int OTHER 6
public static final int SINGLE_COMMENT 10
public static final int SINGLE_COMMENT_JML 11
public static final int STRING 5
public static final int WHITE 1
public static final int WORD 0

jack.plugin.perspective.ICaseExplorer
public static final int FLAT 0
public static final int HIERARCHY 1

jack.plugin.prove.ProofTask
public static final int ERROR 7
public static final int FINISHED 1
public static final int LOADING 4
public static final int RUNNING 3
public static final int STARTING 5
public static final int STOPPED 6
public static final int WAITING 2

jml2b.formula.*

jml2b.formula.BasicType
public static final int BOOL 3
public static final int FUNC 5
public static final int PROP 2
public static final int REF 1
public static final int TYPES 4
public static final int Z 0

jml2b.formula.IFormToken
public static final byte ARRAY_ACCESS 65
public static final byte ARRAY_RANGE 53
public static final byte B_ACCOLADE 33
public static final byte B_APPLICATION 41
public static final byte B_ARRAY_EQUALS 68
public static final byte B_BOOL 43
public static final byte B_BTRUE 32
public static final byte B_COUPLE 44
public static final byte B_DOM 54
public static final byte B_FUNCTION_EQUALS 57
public static final byte B_IN 42
public static final byte B_INTERVAL 39
public static final byte B_OVERRIDING 34
public static final byte B_SET_EQUALS 55
public static final byte B_SUBSTRACTION_DOM 56
public static final byte B_UNION 35
public static final byte CONSTANT_FUNCTION 37
public static final byte CONSTANT_FUNCTION_FUNCTION 58
public static final byte EQUALS_ON_OLD_INSTANCES 47
public static final byte EQUALS_ON_OLD_INSTANCES_ARRAY 62
public static final byte FINAL_IDENT 48
public static final byte GUARDED_SET 51
public static final byte INTERSECTION_IS_NOT_EMPTY 52
public static final byte IS_ARRAY 38
public static final byte IS_MEMBER_FIELD 45
public static final byte IS_STATIC_FIELD 64
public static final byte Ja_ADD_OP 0
public static final byte Ja_AND_OP 2
public static final byte Ja_CHAR_LITERAL 15
public static final byte Ja_COMMA 7
public static final byte Ja_DIFFERENT_OP 21
public static final byte Ja_DIV_OP 25
public static final byte Ja_EQUALS_OP 1
public static final byte Ja_GE_OP 23
public static final byte Ja_GREATER_OP 24
public static final byte Ja_IDENT 6
public static final byte Ja_JAVA_BUILTIN_TYPE 16
public static final byte Ja_LE_OP 4
public static final byte Ja_LESS_OP 22
public static final byte Ja_LITERAL_false 12
public static final byte Ja_LITERAL_null 13
public static final byte Ja_LITERAL_super 17
public static final byte Ja_LITERAL_this 8
public static final byte Ja_LITERAL_true 11
public static final byte Ja_LNOT 10
public static final byte Ja_MOD 9
public static final byte Ja_MUL_OP 3
public static final byte Ja_NEGATIVE_OP 19
public static final byte Ja_NUM_INT 14
public static final byte Ja_OR_OP 20
public static final byte Ja_QUESTION 26
public static final byte Ja_STRING_LITERAL 18
public static final byte Ja_UNARY_NUMERIC_OP 5
public static final byte Jm_AND_THEN 66
public static final byte Jm_EXISTS 46
public static final byte Jm_FORALL 36
public static final byte Jm_IMPLICATION_OP 28
public static final byte Jm_IS_SUBTYPE 31
public static final byte Jm_OR_ELSE 67
public static final byte Jm_T_OLD 29
public static final byte Jm_T_RESULT 27
public static final byte Jm_T_TYPE 30
public static final byte LOCAL_ELEMENTS_DECL 69
public static final byte LOCAL_VAR_DECL 50
public static final byte MODIFIED_FIELD 59
public static final byte NEW_OBJECT 61
public static final byte T_CALLED_OLD 49
public static final byte T_TYPE 63
public static final byte T_VARIANT_OLD 60

jml2b.link.*

jml2b.link.Linkable
public static final int STATE_LINKED 1
public static final int STATE_LINKED_STATEMENTS 2
public static final int STATE_LINKED_TYPE_CHECKED 3
public static final int STATE_UNLINKED 0

jml2b.link.LinkInfo
public static final int PACKAGE 2
public static final int TYPE 1

jml2b.pog.*

jml2b.pog.lemma.GoalOrigin
public static final byte ASSERT 9
public static final byte BLOCK_ENSURES 12
public static final byte BLOCK_EXSURES 11
public static final byte BLOCK_REQUIRES 10
public static final byte ENSURES 2
public static final byte EXSURES 5
public static final byte INSTANCE_CONSTRAINT 16
public static final byte LOOP_EXSURES 6
public static final byte LOOP_INVARIANT_INIT 4
public static final byte LOOP_INVARIANT_PRESERVE 17
public static final byte LOOP_VARIANT 13
public static final byte MEMBER_INVARIANT 1
public static final byte MODIFIES 7
public static final byte REQUIRES 3
public static final byte STATIC_CONSTRAINT 15
public static final byte STATIC_INVARIANT 0
public static final byte SUPER_REQUIRES 8
public static final byte WELL_DEFINED 14

jml2b.pog.lemma.ProverStatus
public static final byte PROVED 1
public static final byte UNPROVED 0

jml2b.pog.lemma.VirtualFormula
public static final byte ASSERT 2
public static final byte BLOCK_ENSURES 7
public static final byte BLOCK_EXSURES 8
public static final byte ENSURES 3
public static final byte EXSURES 4
public static final byte GOAL 11
public static final byte INVARIANT 9
public static final byte LOCALES 1
public static final byte LOOP_EXSURES 6
public static final byte LOOP_INVARIANT 5
public static final byte REQUIRES 0
public static final byte STATIC_FINAL_FIELDS_INVARIANT 10

jml2b.pog.substitution.Substitution
public static final byte ARRAY_ELEMENT 0
public static final byte ARRAY_ELEMENT_SINGLE 9
public static final byte ARRAY_LENGTH 1
public static final byte FORM 2
public static final byte INSTANCES_SET 3
public static final byte INSTANCES_SINGLE 4
public static final byte MEMBER_FIELD 8
public static final byte TMP_VAR 5
public static final byte TYPEOF_SET 6
public static final byte TYPEOF_SINGLE 7

jml2b.pog.util.ColoredInfo
public static final byte EQUALS_0 14
public static final byte IS_FALSE 2
public static final byte IS_NEGATIVE 12
public static final byte IS_NOT_CASTABLE 11
public static final byte IS_NOT_STORABLE 15
public static final byte IS_NULL 13
public static final byte IS_OUT_OF_BOUNDS 16
public static final byte IS_TRUE 1
public static final byte METHOD_CALL 21
public static final byte NEW 22
public static final byte THROWS_EXCEPTION 17

jml2b.structure.*

jml2b.structure.java.Identifier
public static final int ID_CLASS 1
public static final int ID_FIELD 5
public static final int ID_METHOD 4
public static final int ID_PACKAGE 2
public static final int ID_UNKNOWN 0

jml2b.structure.java.JmlFile
public static final int JPO_FILE_FORMAT_VERSION 29

jml2b.structure.java.ModFlags
public static final int ABSTRACT 2
public static final int FINAL 1
public static final int GHOST 2048
public static final int MODEL 4096
public static final int NATIVE 512
public static final int NON_NULL 64
public static final int PRIVATE 8
public static final int PROTECTED 16
public static final int PUBLIC 4
public static final int PURE 128
public static final int SPEC_PUBLIC 256
public static final int STATIC 32
public static final int SYNCHRONIZED 1024

jml2b.structure.java.Type
public static final int T_ARRAY 7
public static final int T_BOOLEAN 4
public static final int T_BYTE 3
public static final int T_CHAR 5
public static final int T_CLASS 14
public static final int T_DOUBLE 11
public static final int T_FLOAT 9
public static final int T_INT 1
public static final int T_LONG 10
public static final int T_NULL 12
public static final int T_REF 6
public static final int T_SHORT 2
public static final int T_TYPE 13
public static final int T_VOID 8

jml2b.structure.jml.SpecCase
public static final int DEFAULT_BEHAVIOR_CASE 3
public static final int EXCEPTIONAL_BEHAVIOR_CASE 2
public static final int LIGHTWEIGHT_CASE 0
public static final int NORMAL_BEHAVIOR_CASE 1

jml2b.structure.statement.MyToken
public static final int BTRUE 369
public static final int FIRST_TOKEN 367
public static final int METHOD_CALL 370
public static final int NEWARRAY 371
public static final int SEQUENCE 367
public static final int SKIP 368
public static final int T_CALLED_OLD 372
public static final int T_FRESH_CALLED_OLD 373
public static final int T_VARIANT_OLD 374

jml2b.util.*

jml2b.util.Tabs
public static final int DEFAULT_TAB_SIZE 4

jpov.*

jpov.Icons
public static final int PROVED_IMAGES_COUNT 3

Overview  Package  Class  Use  Tree  Deprecated  Index  Help 
 PREV   NEXT FRAMES    NO FRAMES