jml2b.structure.jml
Class SpecCase

java.lang.Object
  jml2b.util.Profiler
      jml2b.structure.java.ParsedItem
          jml2b.structure.jml.SpecCase

All Implemented Interfaces:

jml.JmlDeclParserTokenTypes, Linkable, java.io.Serializable, TypeCheckable

public class SpecCase

extends ParsedItem

implements Linkable, TypeCheckable, java.io.Serializable, jml.JmlDeclParserTokenTypes

This class implements a specification case, that is a labelled record of requires, modifies, ensures and exsures.

Author:

L. Burdy, A. Requet

See Also:

Serialized Form

Field Summary

static int	DEFAULT_BEHAVIOR_CASE Constant corresponding to default behavior cases.
static int	EXCEPTIONAL_BEHAVIOR_CASE Constant corresponding to exceptional_behavior cases.
static int	LIGHTWEIGHT_CASE Constant corresponding to lightweight cases.
static int	NORMAL_BEHAVIOR_CASE Constant corresponding to normal behavior cases.

Fields inherited from interface jml2b.link.Linkable

STATE_LINKED, STATE_LINKED_STATEMENTS, STATE_LINKED_TYPE_CHECKED, STATE_UNLINKED

Fields inherited from interface jml.JmlDeclParserTokenTypes

ABRUPT_BEHAVIOR, ACCESSIBLE, ACCESSIBLE_KEYWORD, ACCESSIBLE_REDUNDANTLY, ACCESSIBLE_SEQ, ADDITIVE_ASSIGNMENT_OP, ADDITIVE_OP, AFFIRM_KEYWORD, ALSO, AND, ARRAY_DECLARATOR, ASGNABLE_SEQ, ASSERT, ASSERT_REDUNDANTLY, ASSIGN, ASSIGNABLE, ASSIGNABLE_KEYWORD, ASSIGNABLE_REDUNDANTLY, ASSUME, ASSUME_KEYWORD, ASSUME_REDUNDANTLY, AXIOM, BACKWARD_IMPLIES, BADCHAR, BAND, BAND_ASSIGN, BEHAVIOR, BITWISE_ASSIGNMENT_OP, BITWISE_OP, BNOT, BOR, BOR_ASSIGN, BREAKS, BREAKS_KEYWORD, BREAKS_REDUNDANTLY, BREAKS_SEQ, BSR, BSR_ASSIGN, BXOR, BXOR_ASSIGN, CALLABLE, CALLABLE_KEYWORD, CALLABLE_REDUNDANTLY, CALLABLE_SEQ, CASE, CAST, CHAR_LITERAL, CHOOSE, CHOOSE_IF, COLON, COMMA, CONJOINABLE_SPEC, CONSTRAINT, CONSTRAINT_KEYWORD, CONSTRAINT_REDUNDANTLY, CONSTRUCTOR, CONT_SEQ, CONTINUES, CONTINUES_KEYWORD, CONTINUES_REDUNDANTLY, DEC, DECREASES, DECREASES_REDUNDANTLY, DECREASING, DECREASING_KEYWORD, DECREASING_REDUNDANTLY, DEPENDS, DEPENDS_KEYWORD, DEPENDS_REDUNDANTLY, DIM_EXPRS, DIMS, DINFORMALLY, DIV, DIV_ASSIGN, DIV_SEQ, DIVERGES, DIVERGES_KEYWORD, DIVERGES_REDUNDANTLY, DOC_ATSIGN, DOC_ATSIGN_KEYWORD, DOC_AUTHOR, DOC_COMMENT, DOC_COMMENT_START, DOC_DEPRECATED, DOC_EXCEPTION, DOC_JML_SPECS, DOC_NL_WS, DOC_NON_EMPTY_TEXTLINE, DOC_NON_NL_WS, DOC_PARAM, DOC_RETURN, DOC_SEE, DOC_SERIAL, DOC_SERIALDATA, DOC_SERIALFIELD, DOC_SINCE, DOC_THROWS, DOC_UNKNOWN_KEYWORD, DOC_VERSION, DOT, DOT_DOT, ELSE, ENS_SEQ, ENSURES, ENSURES_KEYWORD, ENSURES_REDUNDANTLY, EOF, EQUAL, EQUALITY_OP, EQUIV, EQUIVALENCE_OP, ESC, EXAMPLE, EXCEPTIONAL_BEHAVIOR, EXCEPTIONAL_EXAMPLE, EXPONENT, EXSURES, EXSURES_REDUNDANTLY, EXT_ALSO, EXT_AND, FLOAT_SUFFIX, FOR, FOR_EXAMPLE, FOR_INIT, FOR_TEST, FOR_UPDATER, FORALL, GE, GHOST, GT, HENCE_BY, HENCE_BY_KEYWORD, HENCE_BY_REDUNDANTLY, HEX_DIGIT, IDENT, IGNORED_AT_IN_COMMENT, IMPLICATION_OP, IMPLIES_THAT, INC, INFORMAL_DESCRIPTION, INIT, INITIALIZER, INITIALLY, INSTANCE, INSTANCE_INIT, INVARIANT, INVARIANT_KEYWORD, INVARIANT_REDUNDANTLY, IS_SUBTYPE_OF, JAVA_BUILTIN_TYPE, JAVA_MODIFIER, JML_BACKSLASH_SEQUENCE, JML_MODIFIER, L_ARROW, LABEL, LABEL_KEYWORD, LAND, LBRACK, LCURLY, LCURLY_VBAR, LE, LET, LETOLD_KEYWORD, LIMPLIES, LITERAL_abstract, LITERAL_assert, LITERAL_boolean, LITERAL_break, LITERAL_byte, LITERAL_case, LITERAL_catch, LITERAL_char, LITERAL_class, LITERAL_const, LITERAL_continue, LITERAL_default, LITERAL_do, LITERAL_double, LITERAL_else, LITERAL_extends, LITERAL_false, LITERAL_final, LITERAL_finally, LITERAL_float, LITERAL_for, LITERAL_if, LITERAL_implements, LITERAL_import, LITERAL_instanceof, LITERAL_int, LITERAL_interface, LITERAL_long, LITERAL_native, LITERAL_new, LITERAL_null, LITERAL_package, LITERAL_private, LITERAL_protected, LITERAL_public, LITERAL_return, LITERAL_short, LITERAL_static, LITERAL_strictfp, LITERAL_super, LITERAL_switch, LITERAL_synchronized, LITERAL_this, LITERAL_throw, LITERAL_throws, LITERAL_transient, LITERAL_true, LITERAL_try, LITERAL_void, LITERAL_volatile, LITERAL_while, LNOT, LOGICAL_OP, LOOP_ASGNABLE_SEQ, LOOP_ASSIGNABLE_KEYWORD, LOOP_EXSURES, LOOP_INV_SEQ, LOOP_INVARIANT, LOOP_INVARIANT_REDUNDANTLY, LOOP_MODIFIES, LOOP_SIG_SEQ, LOR, LPAREN, LT, MAINTAINING, MAINTAINING_KEYWORD, MAINTAINING_REDUNDANTLY, MEASURED_BY, MEASURED_BY_KEYWORD, MEASURED_BY_REDUNDANTLY, METH, MINUS, MINUS_ASSIGN, ML_COMMENT, MOD, MOD_ASSIGN, MODEL, MODEL_PROGRAM, MODIFIABLE, MODIFIABLE_REDUNDANTLY, MODIFIER_SET, MODIFIES, MODIFIES_REDUNDANTLY, MONITORED, MONITORED_BY, MULTIPLICATIVE_ASSIGNMENT_OP, MULTIPLICATIVE_OP, NESTED_CLASS, NL_WS, NON_NL_WS, NON_NULL, NORMAL_BEHAVIOR, NORMAL_EXAMPLE, NOT_EQUAL, NOT_EQUIV, NOWARN_LABEL, NOWARN_LABEL_LIST, NULL_TREE_LOOKAHEAD, NUM_FLOAT, NUM_INT, OLD, OR, PARAM, PLUS, PLUS_ASSIGN, POST, POST_DEC, POST_INC, POST_INCREMENT_OP, POST_REDUNDANTLY, PRE, PRE_INCREMENT_OP, PRE_REDUNDANTLY, PRIVACY_MODIFIER, PURE, QUANT_VARS, QUANTIFIED_EXPR, QUANTIFIER_TOKEN, QUESTION, R_ARROW, RBRACK, RCURLY, READABLE_IF, REFINE, RELATIONAL_OP, REPLACE, REPRESENTS, REPRESENTS_KEYWORD, REPRESENTS_REDUNDANTLY, REQUIRES, REQUIRES_KEYWORD, REQUIRES_REDUNDANTLY, RETURNS, RETURNS_KEYWORD, RETURNS_REDUNDANTLY, RETURNS_SEQ, RPAREN, SEMI, SET, SET_COMPR, SHIFT_ASSIGNMENT_OP, SHIFT_OP, SIG_SEQ, SIGNALS, SIGNALS_KEYWORD, SIGNALS_REDUNDANTLY, SL, SL_ASSIGN, SL_COMMENT, SPEC_CASE, SPEC_PROTECTED, SPEC_PUBLIC, SPEC_SL_COMMENT, SPEC_STATEMENT, SR, SR_ASSIGN, STAR, STAR_ASSIGN, STAR_ELEMS, STATIC_INITIALIZER, STRING_LITERAL, SUBCLASSING_CONTRACT, T_ELEMTYPE, T_EVERYTHING, T_EXISTS, T_FIELDS_OF, T_FORALL, T_FRESH, T_INVARIANT_FOR, T_IS_INITIALIZED, T_LBLNEG, T_LBLPOS, T_LOCKSET, T_MAX, T_MIN, T_NONNULLELEMENTS, T_NOT_MODIFIED, T_NOT_SPECIFIED, T_NOTHING, T_NUM_OF, T_OLD, T_OTHER, T_PRODUCT, T_REACH, T_RESULT, T_SUCH_THAT, T_SUM, T_TYPE, T_TYPEOF, T_TYPEOFALLTYPES, UNARY_NUMERIC_OP, UNINITIALIZED, UNREACHABLE, VAR_DECL, VBAR_RCURLY, VF_SEQ, VOCAB, WEAKLY, WHEN, WHEN_KEYWORD, WHEN_REDUNDANTLY, WS

Constructor Summary

SpecCase()

SpecCase(Expression ens, ModifiesClause mod)

SpecCase(IJml2bConfiguration config)
Construct an empty spec case.

SpecCase(IJml2bConfiguration config, LinkContext f)
Construct and link an empty by default spec case.

SpecCase(IJml2bConfiguration config, Modifiers mods)

Method Summary

boolean	addAnnotation(IJml2bConfiguration config, Expression ens, ModifiesClause mod)
void	addAnnotation(IJml2bConfiguration config, SpecCase sc)
boolean	addComputedModifies(IJml2bConfiguration config, ModifiesList ml)
void	addUnlinkedExsuresFalse(java.lang.String fqn) Add a exsure false clause for the given exception type fqn.
java.lang.Object	clone()
void	completeModifiesWithOwnFields(ModifiesList l) Complete the modifies clause of a constructor with the fields of the class.
void	completeSpecCase(IJml2bConfiguration config, Expression req, java.util.Vector labels, Modifiers mods, Modifiers methodMods, int type) Completes the modifies, if no modifies were declared, the modifies becomes a modifies \everything
java.lang.String	emit(IJml2bConfiguration config)
static void	exsureVectorInstancie(java.util.Enumeration ex) Instancie the exsures clause.
static void	exsureVectorProcessIdent(java.util.Enumeration ex) Collects all the indentifier of the exsures clause to give them an index in the identifer array.
static void	exsureVectorRenameParam(java.util.Enumeration ex, Parameters signature, Parameters newSignature)
Expression	getEnsures() Returns the content of the ensures clause.
java.util.Enumeration	getExsures() Returns an Enumeration enumerating the content of the exsures clause.
Expression	getExsuresAsExpression()
java.lang.String	getInfo() Returns the Java informations corresponding to this case
java.util.Vector	getLabels() Returns the labels.
IModifiers	getModifiers() Returns the modifier associated to this SpecCase.
ModifiesClause	getModifies() Returns the content of the modifies clause.
Expression	getNormalizedEnsures() Returns the ensures clause guarded by the requires clause
Expression	getRequires() Returns the content of the requires clause.
boolean	hasExsures() Return true if the current spec case has an exsure clause defined.
void	jmlNormalize(IJml2bConfiguration config, Class definingClass) Normalize the specification case.
void	link(IJml2bConfiguration config, LinkContext f)
int	linkStatements(IJml2bConfiguration config, LinkContext f)
SimpleLemma	modifiesLemmas(IJml2bConfiguration config, java.util.Vector fields) Returns the lemmas concerning the proof of the modifies clause.
int	parseEnsures(JmlFile jmlFile, antlr.collections.AST a, int first_line) Parses the content of the ensures clause, and returns the new value for first_line.
int	parseExsures(JmlFile jmlFile, antlr.collections.AST a, int first_line) Parse the content of an exsures clause, returning the new value for first_line.
static void	parseLabel(java.util.Vector labels, antlr.collections.AST a, JmlFile jmlFile) Parses the label clause of a specification case.
int	parseModifies(JmlFile jmlFile, antlr.collections.AST a, int first_line) Parses the modifies clause, and returns the updated value of first_line.
antlr.collections.AST	parseSpecBlock(JmlFile file, antlr.collections.AST tree) Parses the content of a lightweight spec case.
void	renameParam(IJml2bConfiguration config, Parameters signature, Parameters newSignature)
void	setEnsures(Expression expression)
void	setExsure(java.util.Vector vector)
void	setModifiers(Modifiers mods) Sets the modifiers for the current SpecCase object.
void	setModifies(ModifiesClause clause)
void	setParsedItem(ParsedItem pi)
void	setRequires(Expression expression)
Type	typeCheck(IJml2bConfiguration config, LinkContext f)

Methods inherited from class jml2b.structure.java.ParsedItem

change, change, getColumn, getJmlFile, getLine, save, setBox

Methods inherited from class jml2b.util.Profiler

runGC

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

LIGHTWEIGHT_CASE

public static final int LIGHTWEIGHT_CASE

Constant corresponding to lightweight cases.

See Also:

Constant Field Values

NORMAL_BEHAVIOR_CASE

public static final int NORMAL_BEHAVIOR_CASE

Constant corresponding to normal behavior cases.

See Also:

Constant Field Values

EXCEPTIONAL_BEHAVIOR_CASE

public static final int EXCEPTIONAL_BEHAVIOR_CASE

Constant corresponding to exceptional_behavior cases.

See Also:

Constant Field Values

DEFAULT_BEHAVIOR_CASE

public static final int DEFAULT_BEHAVIOR_CASE

Constant corresponding to default behavior cases.

See Also:

Constant Field Values

Constructor Detail

SpecCase

public SpecCase(IJml2bConfiguration config,
                Modifiers mods)
         throws Jml2bException

SpecCase

public SpecCase(IJml2bConfiguration config)

Construct an empty spec case.

SpecCase

public SpecCase()

SpecCase

public SpecCase(IJml2bConfiguration config,
                LinkContext f)
         throws Jml2bException

Construct and link an empty by default spec case.

Parameters:

config - The current configuration

f - The current link context

SpecCase

public SpecCase(Expression ens,
                ModifiesClause mod)

Method Detail

exsureVectorProcessIdent

public static void exsureVectorProcessIdent(java.util.Enumeration ex)

Collects all the indentifier of the exsures clause to give them an index in the identifer array. This array is then analyzed to give short name when it is possible to identifiers.

See Also:

jml2b.pog.IdentifierResolver#bIdents

exsureVectorInstancie

public static void exsureVectorInstancie(java.util.Enumeration ex)

Instancie the exsures clause. More informations on instancie.

exsureVectorRenameParam

public static void exsureVectorRenameParam(java.util.Enumeration ex,
                                           Parameters signature,
                                           Parameters newSignature)

parseLabel

public static void parseLabel(java.util.Vector labels,
                              antlr.collections.AST a,
                              JmlFile jmlFile)
                       throws Jml2bException

Parses the label clause of a specification case.

Parameters:

labels - The set of labels to constructs

a - The currently parsed AST tree

jmlFile - The currently parsed JML file

Throws:

Jml2bException

clone

public java.lang.Object clone()

parseSpecBlock

public antlr.collections.AST parseSpecBlock(JmlFile file,
                                            antlr.collections.AST tree)
                                     throws Jml2bException

Parses the content of a lightweight spec case. The spec case is assumed not to contain subcases.

Throws:

Jml2bException

hasExsures

public boolean hasExsures()

Return true if the current spec case has an exsure clause defined.

completeSpecCase

public void completeSpecCase(IJml2bConfiguration config,
                             Expression req,
                             java.util.Vector labels,
                             Modifiers mods,
                             Modifiers methodMods,
                             int type)
                      throws Jml2bException

Completes the modifies, if no modifies were declared, the modifies becomes a modifies \everything

Throws:

Jml2bException

addUnlinkedExsuresFalse

public void addUnlinkedExsuresFalse(java.lang.String fqn)

Add a exsure false clause for the given exception type fqn. This method should be called before the SpecCase is linked, since it adds unlinked elements.

Parameters:

fqn - the fully qualified name of the exception type.

link

public void link(IJml2bConfiguration config,
                 LinkContext f)
          throws Jml2bException

Specified by:

link in interface Linkable

Throws:

Jml2bException

See Also:

Linkable.link(IJml2bConfiguration, LinkContext)

linkStatements

public int linkStatements(IJml2bConfiguration config,
                          LinkContext f)
                   throws Jml2bException

Specified by:

linkStatements in interface Linkable

Throws:

Jml2bException

See Also:

Linkable.linkStatements(IJml2bConfiguration, LinkContext)

typeCheck

public Type typeCheck(IJml2bConfiguration config,
                      LinkContext f)
               throws Jml2bException

Specified by:

typeCheck in interface TypeCheckable

Throws:

Jml2bException

parseExsures

public int parseExsures(JmlFile jmlFile,
                        antlr.collections.AST a,
                        int first_line)
                 throws Jml2bException

Parse the content of an exsures clause, returning the new value for first_line.

Throws:

Jml2bException

parseEnsures

public int parseEnsures(JmlFile jmlFile,
                        antlr.collections.AST a,
                        int first_line)
                 throws Jml2bException

Parses the content of the ensures clause, and returns the new value for first_line.

Throws:

Jml2bException

parseModifies

public int parseModifies(JmlFile jmlFile,
                         antlr.collections.AST a,
                         int first_line)
                  throws Jml2bException

Parses the modifies clause, and returns the updated value of first_line.

Throws:

Jml2bException

jmlNormalize

public void jmlNormalize(IJml2bConfiguration config,
                         Class definingClass)
                  throws PogException

Normalize the specification case. Ensures that processIdent and instancie are called for each of the clause. If no modifies is set, set it to \modifieseverything. Adds the dependees to the modifies list.

Throws:

PogException

renameParam

public void renameParam(IJml2bConfiguration config,
                        Parameters signature,
                        Parameters newSignature)
                 throws PogException

Throws:

PogException

completeModifiesWithOwnFields

public void completeModifiesWithOwnFields(ModifiesList l)

Complete the modifies clause of a constructor with the fields of the class.

Parameters:

l -

getInfo

public java.lang.String getInfo()

Returns the Java informations corresponding to this case

Returns:

a string to be displayed as tooltip text in the viewer.

getNormalizedEnsures

public Expression getNormalizedEnsures()

Returns the ensures clause guarded by the requires clause

getExsuresAsExpression

public Expression getExsuresAsExpression()

modifiesLemmas

public SimpleLemma modifiesLemmas(IJml2bConfiguration config,
                                  java.util.Vector fields)
                           throws PogException

Returns the lemmas concerning the proof of the modifies clause.

Parameters:

config - The current configuration

fields - The set of modifiable fields

Throws:

PogException

getLabels

public java.util.Vector getLabels()

Returns the labels.

Returns:

Vector

getEnsures

public Expression getEnsures()

Returns the content of the ensures clause.

getExsures

public java.util.Enumeration getExsures()

Returns an Enumeration enumerating the content of the exsures clause. The elements returned by the Enumeration object will be of type Exsures.

getRequires

public Expression getRequires()

Returns the content of the requires clause.

getModifies

public ModifiesClause getModifies()

Returns the content of the modifies clause.

getModifiers

public IModifiers getModifiers()

Returns the modifier associated to this SpecCase. Returns null if no modifier is available.

setModifiers

public void setModifiers(Modifiers mods)

Sets the modifiers for the current SpecCase object.

emit

public java.lang.String emit(IJml2bConfiguration config)

setParsedItem

public void setParsedItem(ParsedItem pi)

addAnnotation

public void addAnnotation(IJml2bConfiguration config,
                          SpecCase sc)

addAnnotation

public boolean addAnnotation(IJml2bConfiguration config,
                             Expression ens,
                             ModifiesClause mod)

addComputedModifies

public boolean addComputedModifies(IJml2bConfiguration config,
                                   ModifiesList ml)

setEnsures

public void setEnsures(Expression expression)

Parameters:

expression -

setExsure

public void setExsure(java.util.Vector vector)

Parameters:

vector -

setModifies

public void setModifies(ModifiesClause clause)

Parameters:

clause -

setRequires

public void setRequires(Expression expression)

Parameters:

expression -