JML

org.jmlspecs.checker
Class JmlMessages

java.lang.Object
  extended byorg.jmlspecs.checker.JmlMessages

public class JmlMessages
extends Object


Field Summary
static MessageDescription ADMISSIBILITY_METHOD_CALL_NOT_SUPPORTED
           
static MessageDescription ADMISSIBILITY_OBJECT_CREATION_NOT_SUPPORTED
           
static MessageDescription ADMISSIBILITY_STATICS_NOT_SUPPORTED
           
static MessageDescription AMBIGUOUS_CALLABLE_METHOD
           
static MessageDescription ARITHMETIC_MODE_CONFLICT
           
static MessageDescription ARRAY_NULLITY_DECLARATION_MISMATCH
           
static MessageDescription ASSERTIONS_FOR_MORE_THAN_ONE_VAR
           
static MessageDescription ASSIGNABLE_CHECKING
           
static MessageDescription AXIOM_MODIFIERS
           
static MessageDescription BAD_ABRUPT_SPEC_BODY
           
static MessageDescription BAD_EXCEPTIONAL_SPEC_BODY
           
static MessageDescription BAD_INITIALIZER_MODIFIERS
           
static MessageDescription BAD_NORMAL_SPEC_BODY
           
static MessageDescription BAD_PARAM_MOD_ORDER
           
static MessageDescription BAD_PRIVACY_MODIFIER
           
static MessageDescription BAD_SIMPLE_SPEC_BODY
           
static MessageDescription BAD_SIMPLE_SPEC_STATEMENT_BODY
           
static MessageDescription BAD_SPEC_BODY_ORDER
           
static MessageDescription BAD_STORE_REF_KEYWORD
           
static MessageDescription BAD_TYPE_IN_DECREASING_STATEMENT
           
static MessageDescription BAD_TYPE_IN_DURATION_CLAUSE
           
static MessageDescription BAD_TYPE_IN_MEASURED_CLAUSE
           
static MessageDescription BAD_TYPE_IN_SIGNALS
           
static MessageDescription BAD_TYPE_IN_SIGNALS_ONLY
           
static MessageDescription BAD_TYPE_IN_WORKING_SPACE_CLAUSE
           
static MessageDescription CLASS_AFTER_MEMBER
           
static MessageDescription CLASS_FLAGS
           
static MessageDescription CLASS_LEVEL_NULLABLE_NON_NULL_TOGETHER
           
static MessageDescription CLASS_NAME_REFINING_FILENAME
           
static MessageDescription CLASS_NOT_DEFINED
           
static MessageDescription DATA_GROUP_LOCALITY
           
static MessageDescription DATA_GROUP_NOT_MODEL
           
static MessageDescription DATA_GROUP_VISIBILITY
           
static MessageDescription DIFFERENT_REFINING_ACCESS
           
static MessageDescription DIFFERENT_REFINING_FIELD_TYPE
           
static MessageDescription DUPLICATE_SAME_PREDICATE
           
static MessageDescription DURATION_MUST_CONTAIN_METHOD_CALL
           
static MessageDescription DURATION_NOT_ALLOWED
           
static MessageDescription EQUIVALENCE_TYPE
           
static MessageDescription EXTENDING_SPEC_MODIFIERS
           
static MessageDescription EXTRANEOUS_ALSO
           
static MessageDescription FIELD2_VISIBILITY
           
static MessageDescription FIELD_FLAGS
           
static MessageDescription FIELD_INIT_NOT_IN_JAVA_FILE
           
static MessageDescription FIELD_VISIBILITY
           
static MessageDescription FIELD_WITH_MORE_THAN_ONE_INITIALIZER
           
static MessageDescription FLAG_GHOST_AND_SPEC_PUBLIC
           
static MessageDescription FLAG_INSTANCE_AND_STATIC
           
static MessageDescription FLAG_INSTANCE_WITHOUT_MODEL
           
static MessageDescription FLAG_MODEL_AND_FINAL
           
static MessageDescription FLAG_MODEL_AND_GHOST
           
static MessageDescription FLAG_MODEL_AND_SPEC_PUBLIC
           
static MessageDescription FLAG_SPEC_PROTECTED
           
static MessageDescription FLAG_SPEC_PUBLIC
           
static MessageDescription FLAG_SPEC_PUBLIC_AND_PROTECTED
           
static MessageDescription FLAG_SPEC_PUBLIC_AND_PUBLIC
           
static MessageDescription FRESH_NOT_ALLOWED
           
static MessageDescription GENERIC_SPEC_CASE_MODIFIERS
           
static MessageDescription GHOST_FIELD_ACCESS
           
static MessageDescription ILL_FORMED_SET_COMPREHENSION
           
static MessageDescription ILLEGAL_CODE_MODIFIER
           
static MessageDescription ILLEGAL_MODEL_PROG_STATEMENT
           
static MessageDescription ILLEGAL_SAME_PREDICATE
           
static MessageDescription IMPLICIT_NULLITY
           
static MessageDescription INVALID_EXCLUDEFILES_PATTERN_SYNTAX
           
static MessageDescription INVALID_FIELD_NAME_IN_MAPS_CLAUSE
           
static MessageDescription INVALID_FILE_SUFFIX
           
static MessageDescription INVALID_LOCAL_MODIFIER
           
static MessageDescription INVALID_MAPS_CLAUSE
           
static MessageDescription INVALID_MODEL_FIELD_IN_ASSIGNABLE
           
static MessageDescription INVALID_PARAM_MODIFIER
           
static MessageDescription INVALID_REFINE_FILE_SUFFIX
           
static MessageDescription INVALID_REFINING_MODIFIER
           
static MessageDescription INVALID_REFINING_PARAMETER_NAME
           
static MessageDescription INVALID_REFINING_PARAMETER_NULLITY
           
static MessageDescription INVALID_SELF_REFINEMENT
           
static MessageDescription INVARIANT_FALSE
           
static MessageDescription JAVADOC_FAILURE
           
static MessageDescription JML_DECLARATION_FLAGS
           
static MessageDescription JML_FLAGS_MULTIPLE_PRIVACY
           
static MessageDescription JML_FLAGS_STATIC_AND_INSTANCE
           
static MessageDescription LABEL_UNKNOWN
           
static MessageDescription LHS_OF_ASSIGN_STATEMENT
           
static MessageDescription LHS_OF_SET_STATEMENT
           
static MessageDescription LIGHT_WEIGHTED_EXAMPLE_SPEC
           
static MessageDescription LOOP_STMT_EXPECTED
           
static MessageDescription METHOD2_VISIBILITY
           
static MessageDescription METHOD_BODY_NOT_IN_JAVA_FILE
           
static MessageDescription METHOD_FLAGS
           
static MessageDescription METHOD_MAY_NOT_PURE
           
static MessageDescription METHOD_MODIFIER_MISMATCH
           
static MessageDescription METHOD_NON_NULL_IN_SUPER
           
static MessageDescription METHOD_NOT_DEFINED
           
static MessageDescription METHOD_NOT_PURE
           
static MessageDescription METHOD_SPEC_INCONSISTENT
           
static MessageDescription METHOD_SPEC_PRIVACY
           
static MessageDescription METHOD_VISIBILITY
           
static MessageDescription MISPLACED_DOT_STAR
           
static MessageDescription MISSING_ALSO
           
static MessageDescription MISSING_REFINING_ALSO
           
static MessageDescription MISSING_REPRESENTS
           
static MessageDescription MODEL_FIELD_ACCESS
           
static MessageDescription MODEL_FIELD_WITH_INITIALIZER
           
static MessageDescription MODEL_IN_PREFIX_EXPRESSION
           
static MessageDescription MODEL_LHS_IN_ASSIGNMENT
           
static MessageDescription MODEL_METHOD_WITH_MORE_THAN_ONE_BODY
           
static MessageDescription MONITORED_FOR_STATIC
           
static MessageDescription MULTIPLE_PRIVACY_MODIFIER
           
static MessageDescription MULTIPLE_VAR_DECL
           
static MessageDescription NESTED_ANNOTATION
           
static MessageDescription NESTED_SAME_PREDICATE
           
static MessageDescription NO_ASSIGNABLE
           
static MessageDescription NO_ASSIGNMENT_EXPRESSION
           
static MessageDescription NO_POSTFIX_EXPRESSION
           
static MessageDescription NO_PREFIX_EXPRESSION
           
static MessageDescription NON_MATCHING_PARAMETER_NAME
           
static MessageDescription NON_MODEL_FIELD_NOT_DEFINED
           
static MessageDescription NON_MODEL_METHOD_NOT_DEFINED
           
static MessageDescription NON_PRIVATE_HELPER
           
static MessageDescription NOT_ADMISSIBLE
           
static MessageDescription NOT_ADMISSIBLE_REP_FIELD_PRIVATE
           
static MessageDescription NOT_ADMISSIBLE_REP_METHOD_PRIVATE
           
static MessageDescription NOT_ASSIGNABLE_FIELD
           
static MessageDescription NOT_ASSIGNED_NOT_ALLOWED
           
static MessageDescription NOT_BOOLEAN
           
static MessageDescription NOT_BOOLEAN_IN_ASSUME
           
static MessageDescription NOT_BOOLEAN_IN_QUANTIFIED
           
static MessageDescription NOT_CALLABLE_METHOD
           
static MessageDescription NOT_CLASS_TYPE
           
static MessageDescription NOT_INTEGRAL_EXPRESSION
           
static MessageDescription NOT_JMLTYPE_SET_MEMBER_TYPE
           
static MessageDescription NOT_MODIFIED_NOT_ALLOWED
           
static MessageDescription NOT_NON_ARRAY_REFERENCE_TYPE_IN_FIELDS_OF
           
static MessageDescription NOT_NON_ARRAY_REFERENCE_TYPE_IN_METHOD_NAME
           
static MessageDescription NOT_NON_ARRAY_REFERENCE_TYPE_IN_REACH
           
static MessageDescription NOT_NUMERIC_IN_QUANTIFIED
           
static MessageDescription NOT_REFERENCE_EXPRESSION
           
static MessageDescription NOT_REFERENCE_EXPRESSION_IN_FIELDS_OF
           
static MessageDescription NOT_REFERENCE_EXPRESSION_IN_REACH
           
static MessageDescription NOT_REFERENCE_SET_MEMBER_TYPE
           
static MessageDescription NOT_REFERENCE_TYPE_IN_FIELDS_OF
           
static MessageDescription NOT_REFERENCE_TYPE_IN_INVARIANT_FOR
           
static MessageDescription NOT_REFERENCE_TYPE_IN_REACH
           
static MessageDescription NOT_SUBTYPE_OF_IN_FIELDS_OF
           
static MessageDescription NOT_TYPE_IN_ELEMTYPE
           
static MessageDescription NULLABLE_NON_NULL_TOGETHER
           
static MessageDescription NULLITY_MODIFIERS_FOR_NON_REF_TYPE
           
static MessageDescription OLD_NOT_ALLOWED
           
static MessageDescription ONLY_ACCESSED_NOT_ALLOWED
           
static MessageDescription ONLY_ASSIGNED_NOT_ALLOWED
           
static MessageDescription ONLY_CALLED_NOT_ALLOWED
           
static MessageDescription ONLY_CAPTURED_NOT_ALLOWED
           
static MessageDescription PARAMETER_NULLITY_MISMATCH
           
static MessageDescription PARSING
           
static MessageDescription PRE_NOT_ALLOWED
           
static MessageDescription PURE_AND_ASSIGNABLE
           
static MessageDescription PURE_AND_CALLS_NON_PURE
           
static MessageDescription RECEIVER_IN_ASSIGNABLE
           
static MessageDescription REDUNDANT_REPRESENTS
           
static MessageDescription REDUNDANT_SPEC_MODIFIERS
           
static MessageDescription REFINE_FILE_CYCLE
           
static MessageDescription REFINE_FILE_NOT_FOUND
           
static MessageDescription REFINING_METHOD_RETURN_DIFFERENT
           
static MessageDescription REFINING_METHOD_THROWS_DIFFERENT
           
static MessageDescription REPRESENTS_LOCALITY
           
static MessageDescription REPRESENTS_NOT_MODEL
           
static MessageDescription REPRESENTS_STATIC_FIELD
           
static MessageDescription REPRESENTS_STATIC_LOCALITY
           
static MessageDescription REPRESENTS_TYPE_MISMATCH
           
static MessageDescription RESULT_NOT_ALLOWED
           
static MessageDescription RESULT_VOID
           
static MessageDescription RHS_OF_SET_STATEMENT
           
static MessageDescription SET_COMPREHENSION_TYPE
           
static MessageDescription SET_STATEMENT
           
static MessageDescription SPACE_NOT_ALLOWED
           
static MessageDescription SPEC_DISCARDED_BLOCKEND
           
static MessageDescription SPEC_DISCARDED_SEMI
           
static MessageDescription SUBCLASSING_CONTRACT
           
static MessageDescription SUBTYPE_OF_TYPE
           
static MessageDescription SUPER_NOT_ALLOWED
           
static MessageDescription SYNCHRONIZED_PURE
           
static MessageDescription THIS_NOT_ALLOWED
           
static MessageDescription TYPE2_VISIBILITY
           
static MessageDescription TYPE_IN_FRESH
           
static MessageDescription TYPE_IN_LABELED_EXPRESSION
           
static MessageDescription TYPE_IN_NONNULLELEMENTS
           
static MessageDescription TYPE_IN_SPACE
           
static MessageDescription TYPE_NAME_IN_TYPE_OF_EXPRESSION
           
static MessageDescription TYPE_UNKNOWN
           
static MessageDescription TYPE_VISIBILITY
           
static MessageDescription TYPECHECKING
           
static MessageDescription UNBALANCED_PAREN
           
static MessageDescription UNCAUGHT_EXCEPTION_IN_SIGNALS
           
static MessageDescription UNEXPECTED_NULLITY_ANNOTATION
           
static MessageDescription UNINITIALIZED_OLD_VAR
           
static MessageDescription UNSAFE_ARITHMETIC_OPERATION
           
static MessageDescription UNUSED_METHOD_SPEC
           
static MessageDescription WORKING_SPACE_MUST_CONTAIN_METHOD_CALL
           
static MessageDescription WORKING_SPACE_NOT_ALLOWED
           
 
Constructor Summary
JmlMessages()
           
 
Method Summary
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

UNBALANCED_PAREN

public static final MessageDescription UNBALANCED_PAREN

LOOP_STMT_EXPECTED

public static final MessageDescription LOOP_STMT_EXPECTED

SET_STATEMENT

public static final MessageDescription SET_STATEMENT

LHS_OF_ASSIGN_STATEMENT

public static final MessageDescription LHS_OF_ASSIGN_STATEMENT

LHS_OF_SET_STATEMENT

public static final MessageDescription LHS_OF_SET_STATEMENT

RHS_OF_SET_STATEMENT

public static final MessageDescription RHS_OF_SET_STATEMENT

MODEL_LHS_IN_ASSIGNMENT

public static final MessageDescription MODEL_LHS_IN_ASSIGNMENT

MODEL_IN_PREFIX_EXPRESSION

public static final MessageDescription MODEL_IN_PREFIX_EXPRESSION

REFINE_FILE_NOT_FOUND

public static final MessageDescription REFINE_FILE_NOT_FOUND

CLASS_AFTER_MEMBER

public static final MessageDescription CLASS_AFTER_MEMBER

UNUSED_METHOD_SPEC

public static final MessageDescription UNUSED_METHOD_SPEC

NESTED_ANNOTATION

public static final MessageDescription NESTED_ANNOTATION

ILLEGAL_MODEL_PROG_STATEMENT

public static final MessageDescription ILLEGAL_MODEL_PROG_STATEMENT

BAD_INITIALIZER_MODIFIERS

public static final MessageDescription BAD_INITIALIZER_MODIFIERS

AXIOM_MODIFIERS

public static final MessageDescription AXIOM_MODIFIERS

EXTENDING_SPEC_MODIFIERS

public static final MessageDescription EXTENDING_SPEC_MODIFIERS

INVALID_LOCAL_MODIFIER

public static final MessageDescription INVALID_LOCAL_MODIFIER

INVALID_PARAM_MODIFIER

public static final MessageDescription INVALID_PARAM_MODIFIER

METHOD_MODIFIER_MISMATCH

public static final MessageDescription METHOD_MODIFIER_MISMATCH

GENERIC_SPEC_CASE_MODIFIERS

public static final MessageDescription GENERIC_SPEC_CASE_MODIFIERS

REDUNDANT_SPEC_MODIFIERS

public static final MessageDescription REDUNDANT_SPEC_MODIFIERS

BAD_PRIVACY_MODIFIER

public static final MessageDescription BAD_PRIVACY_MODIFIER

MULTIPLE_PRIVACY_MODIFIER

public static final MessageDescription MULTIPLE_PRIVACY_MODIFIER

MISPLACED_DOT_STAR

public static final MessageDescription MISPLACED_DOT_STAR

BAD_STORE_REF_KEYWORD

public static final MessageDescription BAD_STORE_REF_KEYWORD

BAD_SIMPLE_SPEC_BODY

public static final MessageDescription BAD_SIMPLE_SPEC_BODY

BAD_NORMAL_SPEC_BODY

public static final MessageDescription BAD_NORMAL_SPEC_BODY

BAD_EXCEPTIONAL_SPEC_BODY

public static final MessageDescription BAD_EXCEPTIONAL_SPEC_BODY

BAD_SIMPLE_SPEC_STATEMENT_BODY

public static final MessageDescription BAD_SIMPLE_SPEC_STATEMENT_BODY

BAD_ABRUPT_SPEC_BODY

public static final MessageDescription BAD_ABRUPT_SPEC_BODY

LIGHT_WEIGHTED_EXAMPLE_SPEC

public static final MessageDescription LIGHT_WEIGHTED_EXAMPLE_SPEC

ARITHMETIC_MODE_CONFLICT

public static final MessageDescription ARITHMETIC_MODE_CONFLICT

NO_ASSIGNMENT_EXPRESSION

public static final MessageDescription NO_ASSIGNMENT_EXPRESSION

NO_PREFIX_EXPRESSION

public static final MessageDescription NO_PREFIX_EXPRESSION

NO_POSTFIX_EXPRESSION

public static final MessageDescription NO_POSTFIX_EXPRESSION

FIELD_VISIBILITY

public static final MessageDescription FIELD_VISIBILITY

FIELD2_VISIBILITY

public static final MessageDescription FIELD2_VISIBILITY

METHOD_VISIBILITY

public static final MessageDescription METHOD_VISIBILITY

METHOD2_VISIBILITY

public static final MessageDescription METHOD2_VISIBILITY

TYPE_VISIBILITY

public static final MessageDescription TYPE_VISIBILITY

TYPE2_VISIBILITY

public static final MessageDescription TYPE2_VISIBILITY

METHOD_SPEC_PRIVACY

public static final MessageDescription METHOD_SPEC_PRIVACY

REPRESENTS_STATIC_LOCALITY

public static final MessageDescription REPRESENTS_STATIC_LOCALITY

REPRESENTS_LOCALITY

public static final MessageDescription REPRESENTS_LOCALITY

REPRESENTS_STATIC_FIELD

public static final MessageDescription REPRESENTS_STATIC_FIELD

REPRESENTS_TYPE_MISMATCH

public static final MessageDescription REPRESENTS_TYPE_MISMATCH

REPRESENTS_NOT_MODEL

public static final MessageDescription REPRESENTS_NOT_MODEL

REDUNDANT_REPRESENTS

public static final MessageDescription REDUNDANT_REPRESENTS

DATA_GROUP_VISIBILITY

public static final MessageDescription DATA_GROUP_VISIBILITY

DATA_GROUP_LOCALITY

public static final MessageDescription DATA_GROUP_LOCALITY

DATA_GROUP_NOT_MODEL

public static final MessageDescription DATA_GROUP_NOT_MODEL

CLASS_FLAGS

public static final MessageDescription CLASS_FLAGS

METHOD_FLAGS

public static final MessageDescription METHOD_FLAGS

FIELD_FLAGS

public static final MessageDescription FIELD_FLAGS

MONITORED_FOR_STATIC

public static final MessageDescription MONITORED_FOR_STATIC

FLAG_INSTANCE_AND_STATIC

public static final MessageDescription FLAG_INSTANCE_AND_STATIC

FLAG_SPEC_PUBLIC

public static final MessageDescription FLAG_SPEC_PUBLIC

FLAG_SPEC_PROTECTED

public static final MessageDescription FLAG_SPEC_PROTECTED

FLAG_SPEC_PUBLIC_AND_PROTECTED

public static final MessageDescription FLAG_SPEC_PUBLIC_AND_PROTECTED

FLAG_MODEL_AND_SPEC_PUBLIC

public static final MessageDescription FLAG_MODEL_AND_SPEC_PUBLIC

FLAG_INSTANCE_WITHOUT_MODEL

public static final MessageDescription FLAG_INSTANCE_WITHOUT_MODEL

FLAG_GHOST_AND_SPEC_PUBLIC

public static final MessageDescription FLAG_GHOST_AND_SPEC_PUBLIC

FLAG_MODEL_AND_GHOST

public static final MessageDescription FLAG_MODEL_AND_GHOST

FLAG_MODEL_AND_FINAL

public static final MessageDescription FLAG_MODEL_AND_FINAL

FLAG_SPEC_PUBLIC_AND_PUBLIC

public static final MessageDescription FLAG_SPEC_PUBLIC_AND_PUBLIC

JML_DECLARATION_FLAGS

public static final MessageDescription JML_DECLARATION_FLAGS

JML_FLAGS_STATIC_AND_INSTANCE

public static final MessageDescription JML_FLAGS_STATIC_AND_INSTANCE

JML_FLAGS_MULTIPLE_PRIVACY

public static final MessageDescription JML_FLAGS_MULTIPLE_PRIVACY

NON_PRIVATE_HELPER

public static final MessageDescription NON_PRIVATE_HELPER

NULLITY_MODIFIERS_FOR_NON_REF_TYPE

public static final MessageDescription NULLITY_MODIFIERS_FOR_NON_REF_TYPE

DIFFERENT_REFINING_FIELD_TYPE

public static final MessageDescription DIFFERENT_REFINING_FIELD_TYPE

DIFFERENT_REFINING_ACCESS

public static final MessageDescription DIFFERENT_REFINING_ACCESS

INVALID_REFINING_MODIFIER

public static final MessageDescription INVALID_REFINING_MODIFIER

NON_MODEL_FIELD_NOT_DEFINED

public static final MessageDescription NON_MODEL_FIELD_NOT_DEFINED

NON_MODEL_METHOD_NOT_DEFINED

public static final MessageDescription NON_MODEL_METHOD_NOT_DEFINED

REFINING_METHOD_RETURN_DIFFERENT

public static final MessageDescription REFINING_METHOD_RETURN_DIFFERENT

REFINING_METHOD_THROWS_DIFFERENT

public static final MessageDescription REFINING_METHOD_THROWS_DIFFERENT

NOT_BOOLEAN_IN_ASSUME

public static final MessageDescription NOT_BOOLEAN_IN_ASSUME

SUBTYPE_OF_TYPE

public static final MessageDescription SUBTYPE_OF_TYPE

TYPE_NAME_IN_TYPE_OF_EXPRESSION

public static final MessageDescription TYPE_NAME_IN_TYPE_OF_EXPRESSION

NOT_NON_ARRAY_REFERENCE_TYPE_IN_METHOD_NAME

public static final MessageDescription NOT_NON_ARRAY_REFERENCE_TYPE_IN_METHOD_NAME

NOT_INTEGRAL_EXPRESSION

public static final MessageDescription NOT_INTEGRAL_EXPRESSION

NOT_REFERENCE_EXPRESSION

public static final MessageDescription NOT_REFERENCE_EXPRESSION

NOT_REFERENCE_EXPRESSION_IN_FIELDS_OF

public static final MessageDescription NOT_REFERENCE_EXPRESSION_IN_FIELDS_OF

NOT_REFERENCE_TYPE_IN_FIELDS_OF

public static final MessageDescription NOT_REFERENCE_TYPE_IN_FIELDS_OF

NOT_NON_ARRAY_REFERENCE_TYPE_IN_FIELDS_OF

public static final MessageDescription NOT_NON_ARRAY_REFERENCE_TYPE_IN_FIELDS_OF

NOT_SUBTYPE_OF_IN_FIELDS_OF

public static final MessageDescription NOT_SUBTYPE_OF_IN_FIELDS_OF

BAD_TYPE_IN_MEASURED_CLAUSE

public static final MessageDescription BAD_TYPE_IN_MEASURED_CLAUSE

BAD_TYPE_IN_DECREASING_STATEMENT

public static final MessageDescription BAD_TYPE_IN_DECREASING_STATEMENT

BAD_TYPE_IN_WORKING_SPACE_CLAUSE

public static final MessageDescription BAD_TYPE_IN_WORKING_SPACE_CLAUSE

BAD_TYPE_IN_DURATION_CLAUSE

public static final MessageDescription BAD_TYPE_IN_DURATION_CLAUSE

BAD_TYPE_IN_SIGNALS_ONLY

public static final MessageDescription BAD_TYPE_IN_SIGNALS_ONLY

BAD_TYPE_IN_SIGNALS

public static final MessageDescription BAD_TYPE_IN_SIGNALS

UNCAUGHT_EXCEPTION_IN_SIGNALS

public static final MessageDescription UNCAUGHT_EXCEPTION_IN_SIGNALS

UNINITIALIZED_OLD_VAR

public static final MessageDescription UNINITIALIZED_OLD_VAR

NOT_REFERENCE_EXPRESSION_IN_REACH

public static final MessageDescription NOT_REFERENCE_EXPRESSION_IN_REACH

NOT_REFERENCE_TYPE_IN_REACH

public static final MessageDescription NOT_REFERENCE_TYPE_IN_REACH

NOT_NON_ARRAY_REFERENCE_TYPE_IN_REACH

public static final MessageDescription NOT_NON_ARRAY_REFERENCE_TYPE_IN_REACH

DUPLICATE_SAME_PREDICATE

public static final MessageDescription DUPLICATE_SAME_PREDICATE

NESTED_SAME_PREDICATE

public static final MessageDescription NESTED_SAME_PREDICATE

ILLEGAL_SAME_PREDICATE

public static final MessageDescription ILLEGAL_SAME_PREDICATE

ILLEGAL_CODE_MODIFIER

public static final MessageDescription ILLEGAL_CODE_MODIFIER

NOT_BOOLEAN

public static final MessageDescription NOT_BOOLEAN

MULTIPLE_VAR_DECL

public static final MessageDescription MULTIPLE_VAR_DECL

NOT_BOOLEAN_IN_QUANTIFIED

public static final MessageDescription NOT_BOOLEAN_IN_QUANTIFIED

NOT_NUMERIC_IN_QUANTIFIED

public static final MessageDescription NOT_NUMERIC_IN_QUANTIFIED

SET_COMPREHENSION_TYPE

public static final MessageDescription SET_COMPREHENSION_TYPE

ILL_FORMED_SET_COMPREHENSION

public static final MessageDescription ILL_FORMED_SET_COMPREHENSION

NOT_REFERENCE_SET_MEMBER_TYPE

public static final MessageDescription NOT_REFERENCE_SET_MEMBER_TYPE

NOT_JMLTYPE_SET_MEMBER_TYPE

public static final MessageDescription NOT_JMLTYPE_SET_MEMBER_TYPE

RESULT_VOID

public static final MessageDescription RESULT_VOID

TYPE_IN_NONNULLELEMENTS

public static final MessageDescription TYPE_IN_NONNULLELEMENTS

NOT_TYPE_IN_ELEMTYPE

public static final MessageDescription NOT_TYPE_IN_ELEMTYPE

NOT_REFERENCE_TYPE_IN_INVARIANT_FOR

public static final MessageDescription NOT_REFERENCE_TYPE_IN_INVARIANT_FOR

NOT_CLASS_TYPE

public static final MessageDescription NOT_CLASS_TYPE

TYPE_UNKNOWN

public static final MessageDescription TYPE_UNKNOWN

FRESH_NOT_ALLOWED

public static final MessageDescription FRESH_NOT_ALLOWED

TYPE_IN_FRESH

public static final MessageDescription TYPE_IN_FRESH

TYPE_IN_SPACE

public static final MessageDescription TYPE_IN_SPACE

TYPE_IN_LABELED_EXPRESSION

public static final MessageDescription TYPE_IN_LABELED_EXPRESSION

LABEL_UNKNOWN

public static final MessageDescription LABEL_UNKNOWN

NOT_MODIFIED_NOT_ALLOWED

public static final MessageDescription NOT_MODIFIED_NOT_ALLOWED

NOT_ASSIGNED_NOT_ALLOWED

public static final MessageDescription NOT_ASSIGNED_NOT_ALLOWED

ONLY_ACCESSED_NOT_ALLOWED

public static final MessageDescription ONLY_ACCESSED_NOT_ALLOWED

ONLY_CALLED_NOT_ALLOWED

public static final MessageDescription ONLY_CALLED_NOT_ALLOWED

ONLY_CAPTURED_NOT_ALLOWED

public static final MessageDescription ONLY_CAPTURED_NOT_ALLOWED

ONLY_ASSIGNED_NOT_ALLOWED

public static final MessageDescription ONLY_ASSIGNED_NOT_ALLOWED

OLD_NOT_ALLOWED

public static final MessageDescription OLD_NOT_ALLOWED

PRE_NOT_ALLOWED

public static final MessageDescription PRE_NOT_ALLOWED

SPACE_NOT_ALLOWED

public static final MessageDescription SPACE_NOT_ALLOWED

WORKING_SPACE_NOT_ALLOWED

public static final MessageDescription WORKING_SPACE_NOT_ALLOWED

DURATION_NOT_ALLOWED

public static final MessageDescription DURATION_NOT_ALLOWED

INVALID_FIELD_NAME_IN_MAPS_CLAUSE

public static final MessageDescription INVALID_FIELD_NAME_IN_MAPS_CLAUSE

WORKING_SPACE_MUST_CONTAIN_METHOD_CALL

public static final MessageDescription WORKING_SPACE_MUST_CONTAIN_METHOD_CALL

DURATION_MUST_CONTAIN_METHOD_CALL

public static final MessageDescription DURATION_MUST_CONTAIN_METHOD_CALL

RESULT_NOT_ALLOWED

public static final MessageDescription RESULT_NOT_ALLOWED

THIS_NOT_ALLOWED

public static final MessageDescription THIS_NOT_ALLOWED

SUPER_NOT_ALLOWED

public static final MessageDescription SUPER_NOT_ALLOWED

EQUIVALENCE_TYPE

public static final MessageDescription EQUIVALENCE_TYPE

INVALID_FILE_SUFFIX

public static final MessageDescription INVALID_FILE_SUFFIX

INVALID_EXCLUDEFILES_PATTERN_SYNTAX

public static final MessageDescription INVALID_EXCLUDEFILES_PATTERN_SYNTAX

INVALID_SELF_REFINEMENT

public static final MessageDescription INVALID_SELF_REFINEMENT

INVALID_REFINE_FILE_SUFFIX

public static final MessageDescription INVALID_REFINE_FILE_SUFFIX

REFINE_FILE_CYCLE

public static final MessageDescription REFINE_FILE_CYCLE

CLASS_NAME_REFINING_FILENAME

public static final MessageDescription CLASS_NAME_REFINING_FILENAME

INVALID_REFINING_PARAMETER_NAME

public static final MessageDescription INVALID_REFINING_PARAMETER_NAME

INVALID_REFINING_PARAMETER_NULLITY

public static final MessageDescription INVALID_REFINING_PARAMETER_NULLITY

METHOD_BODY_NOT_IN_JAVA_FILE

public static final MessageDescription METHOD_BODY_NOT_IN_JAVA_FILE

MODEL_METHOD_WITH_MORE_THAN_ONE_BODY

public static final MessageDescription MODEL_METHOD_WITH_MORE_THAN_ONE_BODY

FIELD_WITH_MORE_THAN_ONE_INITIALIZER

public static final MessageDescription FIELD_WITH_MORE_THAN_ONE_INITIALIZER

FIELD_INIT_NOT_IN_JAVA_FILE

public static final MessageDescription FIELD_INIT_NOT_IN_JAVA_FILE

MODEL_FIELD_WITH_INITIALIZER

public static final MessageDescription MODEL_FIELD_WITH_INITIALIZER

EXTRANEOUS_ALSO

public static final MessageDescription EXTRANEOUS_ALSO

MISSING_ALSO

public static final MessageDescription MISSING_ALSO

MISSING_REFINING_ALSO

public static final MessageDescription MISSING_REFINING_ALSO

RECEIVER_IN_ASSIGNABLE

public static final MessageDescription RECEIVER_IN_ASSIGNABLE

NOT_ASSIGNABLE_FIELD

public static final MessageDescription NOT_ASSIGNABLE_FIELD

INVALID_MAPS_CLAUSE

public static final MessageDescription INVALID_MAPS_CLAUSE

INVALID_MODEL_FIELD_IN_ASSIGNABLE

public static final MessageDescription INVALID_MODEL_FIELD_IN_ASSIGNABLE

AMBIGUOUS_CALLABLE_METHOD

public static final MessageDescription AMBIGUOUS_CALLABLE_METHOD

NOT_CALLABLE_METHOD

public static final MessageDescription NOT_CALLABLE_METHOD

PURE_AND_ASSIGNABLE

public static final MessageDescription PURE_AND_ASSIGNABLE

PURE_AND_CALLS_NON_PURE

public static final MessageDescription PURE_AND_CALLS_NON_PURE

SYNCHRONIZED_PURE

public static final MessageDescription SYNCHRONIZED_PURE

JAVADOC_FAILURE

public static final MessageDescription JAVADOC_FAILURE

NULLABLE_NON_NULL_TOGETHER

public static final MessageDescription NULLABLE_NON_NULL_TOGETHER

CLASS_LEVEL_NULLABLE_NON_NULL_TOGETHER

public static final MessageDescription CLASS_LEVEL_NULLABLE_NON_NULL_TOGETHER

MODEL_FIELD_ACCESS

public static final MessageDescription MODEL_FIELD_ACCESS

GHOST_FIELD_ACCESS

public static final MessageDescription GHOST_FIELD_ACCESS

CLASS_NOT_DEFINED

public static final MessageDescription CLASS_NOT_DEFINED

METHOD_NOT_DEFINED

public static final MessageDescription METHOD_NOT_DEFINED

MISSING_REPRESENTS

public static final MessageDescription MISSING_REPRESENTS

METHOD_SPEC_INCONSISTENT

public static final MessageDescription METHOD_SPEC_INCONSISTENT

INVARIANT_FALSE

public static final MessageDescription INVARIANT_FALSE

ASSERTIONS_FOR_MORE_THAN_ONE_VAR

public static final MessageDescription ASSERTIONS_FOR_MORE_THAN_ONE_VAR

BAD_PARAM_MOD_ORDER

public static final MessageDescription BAD_PARAM_MOD_ORDER

BAD_SPEC_BODY_ORDER

public static final MessageDescription BAD_SPEC_BODY_ORDER

UNSAFE_ARITHMETIC_OPERATION

public static final MessageDescription UNSAFE_ARITHMETIC_OPERATION

SPEC_DISCARDED_SEMI

public static final MessageDescription SPEC_DISCARDED_SEMI

SPEC_DISCARDED_BLOCKEND

public static final MessageDescription SPEC_DISCARDED_BLOCKEND

SUBCLASSING_CONTRACT

public static final MessageDescription SUBCLASSING_CONTRACT

METHOD_NOT_PURE

public static final MessageDescription METHOD_NOT_PURE

NO_ASSIGNABLE

public static final MessageDescription NO_ASSIGNABLE

NON_MATCHING_PARAMETER_NAME

public static final MessageDescription NON_MATCHING_PARAMETER_NAME

METHOD_MAY_NOT_PURE

public static final MessageDescription METHOD_MAY_NOT_PURE

PARAMETER_NULLITY_MISMATCH

public static final MessageDescription PARAMETER_NULLITY_MISMATCH

UNEXPECTED_NULLITY_ANNOTATION

public static final MessageDescription UNEXPECTED_NULLITY_ANNOTATION

METHOD_NON_NULL_IN_SUPER

public static final MessageDescription METHOD_NON_NULL_IN_SUPER

IMPLICIT_NULLITY

public static final MessageDescription IMPLICIT_NULLITY

ARRAY_NULLITY_DECLARATION_MISMATCH

public static final MessageDescription ARRAY_NULLITY_DECLARATION_MISMATCH

PARSING

public static final MessageDescription PARSING

TYPECHECKING

public static final MessageDescription TYPECHECKING

ASSIGNABLE_CHECKING

public static final MessageDescription ASSIGNABLE_CHECKING

NOT_ADMISSIBLE

public static final MessageDescription NOT_ADMISSIBLE

NOT_ADMISSIBLE_REP_FIELD_PRIVATE

public static final MessageDescription NOT_ADMISSIBLE_REP_FIELD_PRIVATE

NOT_ADMISSIBLE_REP_METHOD_PRIVATE

public static final MessageDescription NOT_ADMISSIBLE_REP_METHOD_PRIVATE

ADMISSIBILITY_OBJECT_CREATION_NOT_SUPPORTED

public static final MessageDescription ADMISSIBILITY_OBJECT_CREATION_NOT_SUPPORTED

ADMISSIBILITY_METHOD_CALL_NOT_SUPPORTED

public static final MessageDescription ADMISSIBILITY_METHOD_CALL_NOT_SUPPORTED

ADMISSIBILITY_STATICS_NOT_SUPPORTED

public static final MessageDescription ADMISSIBILITY_STATICS_NOT_SUPPORTED
Constructor Detail

JmlMessages

public JmlMessages()

JML

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.