jml2b.structure.jml
Class ModifiesList

java.lang.Object
  jml2b.util.Profiler
      jml2b.structure.java.ParsedItem
          jml2b.structure.jml.ModifiesClause
              jml2b.structure.jml.ModifiesList

All Implemented Interfaces:

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

public class ModifiesList

extends ModifiesClause

implements jml.JmlDeclParserTokenTypes

This class describes the modifies clause as a list of Modifies elements.

Author:

L. Burdy

See Also:

Serialized Form

Field Summary

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

Fields inherited from interface jml2b.formula.IFormToken

ARRAY_ACCESS, ARRAY_RANGE, B_ACCOLADE, B_APPLICATION, B_ARRAY_EQUALS, B_BOOL, B_BTRUE, B_COUPLE, B_DOM, B_FUNCTION_EQUALS, B_IN, B_INTERVAL, B_OVERRIDING, B_SET_EQUALS, B_SUBSTRACTION_DOM, B_UNION, CONSTANT_FUNCTION, CONSTANT_FUNCTION_FUNCTION, EQUALS_ON_OLD_INSTANCES, EQUALS_ON_OLD_INSTANCES_ARRAY, FINAL_IDENT, GUARDED_SET, INTERSECTION_IS_NOT_EMPTY, IS_ARRAY, IS_MEMBER_FIELD, IS_STATIC_FIELD, Ja_ADD_OP, Ja_AND_OP, Ja_CHAR_LITERAL, Ja_COMMA, Ja_DIFFERENT_OP, Ja_DIV_OP, Ja_EQUALS_OP, Ja_GE_OP, Ja_GREATER_OP, Ja_IDENT, Ja_JAVA_BUILTIN_TYPE, Ja_LE_OP, Ja_LESS_OP, Ja_LITERAL_false, Ja_LITERAL_null, Ja_LITERAL_super, Ja_LITERAL_this, Ja_LITERAL_true, Ja_LNOT, Ja_MOD, Ja_MUL_OP, Ja_NEGATIVE_OP, Ja_NUM_INT, Ja_OR_OP, Ja_QUESTION, Ja_STRING_LITERAL, Ja_UNARY_NUMERIC_OP, Jm_AND_THEN, Jm_EXISTS, Jm_FORALL, Jm_IMPLICATION_OP, Jm_IS_SUBTYPE, Jm_OR_ELSE, Jm_T_OLD, Jm_T_RESULT, Jm_T_TYPE, LOCAL_ELEMENTS_DECL, LOCAL_VAR_DECL, MODIFIED_FIELD, NEW_OBJECT, T_CALLED_OLD, T_TYPE, T_VARIANT_OLD, toString

Constructor Summary

ModifiesList(java.util.Enumeration fields)

ModifiesList(GuardedModifies m, ModifiesList ml)
Constructs a list from a new Modifies element and a list.

ModifiesList(java.util.Iterator fields)

Method Summary

void	add(ModifiesList ml) Concats two lists.
void	addDepends(IJml2bConfiguration config, Class c) Complete the modifies with modified store-ref issued from depends clauses.
boolean	addModifiesWithoutDoublon(IJml2bConfiguration config, GuardedModifies gm)
boolean	addWithoutDoublon(IJml2bConfiguration config, ModifiesList ml)
java.lang.Object	clone() Clones the list.
ModifiesClause	completeModifiesWithFields(ModifiesList l)
java.util.Collection	getFields()
GuardedModifies	getGm()
ModifiesList	getNext()
void	instancie(Expression b, IJml2bConfiguration config) Replace this with the parameter in the modifies clause.
void	instancie(IJml2bConfiguration config) Instancie the modifies clause.
LinkInfo	linkStatements(IJml2bConfiguration config, LinkContext f) Links the content of the clause.
Proofs	modifies(IJml2bConfiguration config, IModifiesField m, Proofs s) Quantifies lemmas and add hypothesis depending on the modified variable list.
SimpleLemma	modifiesLemmas(IJml2bConfiguration config, java.util.Vector fields, java.util.Vector nonModifiedFields, Formula[] nonModifiedxxxElements) Returns the lemmas concerning the proof of the modifies clause for the current method.
void	processIdent() Collects all the indentifier of the clause to give them an index in the identifer array.
ModifiesClause	renameParam(IJml2bConfiguration config, Parameters signature, java.util.Vector newSignature) Renames the parameter in the modifies clause.
void	setParsedItem(ParsedItem pi)
java.lang.String	toJava(int indent) Converts the clause into a string.
Type	typeCheck(IJml2bConfiguration config, LinkContext f)

Methods inherited from class jml2b.structure.jml.ModifiesClause

create

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

Constructor Detail

ModifiesList

public ModifiesList(GuardedModifies m,
                    ModifiesList ml)

Constructs a list from a new Modifies element and a list.

Parameters:

m - The modified variable

ml - The list

ModifiesList

public ModifiesList(java.util.Enumeration fields)

Parameters:

fields -

ModifiesList

public ModifiesList(java.util.Iterator fields)

Method Detail

clone

public java.lang.Object clone()

Clones the list.

Specified by:

clone in class ModifiesClause

Returns:

the cloned list

add

public void add(ModifiesList ml)

Concats two lists.

Parameters:

ml - The list to concat to the current one

addWithoutDoublon

public boolean addWithoutDoublon(IJml2bConfiguration config,
                                 ModifiesList ml)

addModifiesWithoutDoublon

public boolean addModifiesWithoutDoublon(IJml2bConfiguration config,
                                         GuardedModifies gm)

linkStatements

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

Description copied from class: ModifiesClause

Links the content of the clause.

Specified by:

linkStatements in class ModifiesClause

Parameters:

f - context for link

Returns:

the calculated link informations

Throws:

Jml2bException

typeCheck

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

Specified by:

typeCheck in interface TypeCheckable

Throws:

Jml2bException

modifies

public Proofs modifies(IJml2bConfiguration config,
                       IModifiesField m,
                       Proofs s)
                throws PogException

Quantifies lemmas and add hypothesis depending on the modified variable list.

Specified by:

modifies in class ModifiesClause

Parameters:

s - The proof to quantify.

Returns:

The modified proof.

Throws:

PogException

renameParam

public ModifiesClause renameParam(IJml2bConfiguration config,
                                  Parameters signature,
                                  java.util.Vector newSignature)
                           throws PogException

Description copied from class: ModifiesClause

Renames the parameter in the modifies clause.

Specified by:

renameParam in class ModifiesClause

Parameters:

signature - the signature of the called method

newSignature - the list of new names

Returns:

the current modified clause renamed

Throws:

PogException

See Also:

Proofs#renameParam(Parameters, Vector)

instancie

public void instancie(IJml2bConfiguration config)
               throws PogException

Description copied from class: ModifiesClause

Instancie the modifies clause. More informations on instancie.

Specified by:

instancie in class ModifiesClause

Throws:

PogException

instancie

public void instancie(Expression b,
                      IJml2bConfiguration config)
               throws PogException

Description copied from class: ModifiesClause

Replace this with the parameter in the modifies clause.

Specified by:

instancie in class ModifiesClause

Parameters:

b - expression on which the metohd is called.

Throws:

PogException

processIdent

public void processIdent()

Description copied from class: ModifiesClause

Collects all the indentifier of the 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.

Specified by:

processIdent in class ModifiesClause

See Also:

jml2b.pog.IdentifierResolver#bIdents

toJava

public java.lang.String toJava(int indent)

Description copied from class: ModifiesClause

Converts the clause into a string.

Specified by:

toJava in class ModifiesClause

Returns:

the original string reconstructed associated with this clause

modifiesLemmas

public SimpleLemma modifiesLemmas(IJml2bConfiguration config,
                                  java.util.Vector fields,
                                  java.util.Vector nonModifiedFields,
                                  Formula[] nonModifiedxxxElements)
                           throws PogException

Description copied from class: ModifiesClause

Returns the lemmas concerning the proof of the modifies clause for the current method.

Specified by:

modifiesLemmas in class ModifiesClause

Parameters:

config - The current configuration

fields - set of modifiable fields.

nonModifiedFields - The set of formula representing the name of the non modified fields.

nonModifiedxxxElements - The array of Formula representing the name of non modified xxxelements function.

Returns:

goals corresponding to the fact that non declared as modified field are not modifies (a == \old(a)) and that partially declared as modified fields are only partially modified.

Throws:

PogException

addDepends

public void addDepends(IJml2bConfiguration config,
                       Class c)
                throws PogException

Description copied from class: ModifiesClause

Complete the modifies with modified store-ref issued from depends clauses.

Specified by:

addDepends in class ModifiesClause

Parameters:

c - The defining class of the depends clauses

Throws:

PogException

completeModifiesWithFields

public ModifiesClause completeModifiesWithFields(ModifiesList l)

Specified by:

completeModifiesWithFields in class ModifiesClause

Parameters:

l -

Returns:

ModifiesClause

setParsedItem

public void setParsedItem(ParsedItem pi)

Specified by:

setParsedItem in class ModifiesClause

getFields

public java.util.Collection getFields()

Overrides:

getFields in class ModifiesClause

getGm

public GuardedModifies getGm()

Returns:

getNext

public ModifiesList getNext()

Returns: