jml2b.structure.jml
Class ModifiesClause

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

All Implemented Interfaces:

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

Direct Known Subclasses:

ModifiesEverything, ModifiesList, ModifiesNothing

public abstract class ModifiesClause

extends ParsedItem

implements TypeCheckable, jml.JmlDeclParserTokenTypes, IFormToken

This class describes the content of a modifies clause. A modifies clause can be:

• \nothing
• \everything
• a list of modified variable that can be
  • a identifier: a, a.b
  • an array element: a[b]
  • some elements of an array: a[b..c]
  • all the element of an array: a[*]

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

Method Summary

abstract void	addDepends(IJml2bConfiguration config, Class c) Complete the modifies with modified store-ref issued from depends clauses.
abstract java.lang.Object	clone() Clones the object.
abstract ModifiesClause	completeModifiesWithFields(ModifiesList l)
static ModifiesClause	create(JmlFile jf, antlr.collections.AST a) Create a concrete modifies clause depending of the AST content
java.util.Collection	getFields()
abstract void	instancie(Expression b, IJml2bConfiguration config) Replace this with the parameter in the modifies clause.
abstract void	instancie(IJml2bConfiguration config) Instancie the modifies clause.
abstract LinkInfo	linkStatements(IJml2bConfiguration config, LinkContext f) Links the content of the clause.
abstract Proofs	modifies(IJml2bConfiguration config, IModifiesField m, Proofs s) Returns the proof modified in manner to take into account the modifies clause of a called method.
abstract 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.
abstract void	processIdent() Collects all the indentifier of the clause to give them an index in the identifer array.
abstract ModifiesClause	renameParam(IJml2bConfiguration config, Parameters signature, java.util.Vector newSignature) Renames the parameter in the modifies clause.
abstract void	setParsedItem(ParsedItem pi)
abstract java.lang.String	toJava(int indent) Converts the clause into a string.

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

Methods inherited from interface jml2b.link.TypeCheckable

typeCheck

Method Detail

create

public static ModifiesClause create(JmlFile jf,
                                    antlr.collections.AST a)
                             throws Jml2bException

Create a concrete modifies clause depending of the AST content

Parameters:

jf - JML file currently parsed

a - AST tree currently parsed

Returns:

a new concrete modifies clause

Throws:

Jml2bException

clone

public abstract java.lang.Object clone()

Clones the object.

Returns:

the cloned object

instancie

public abstract void instancie(IJml2bConfiguration config)
                        throws PogException

Instancie the modifies clause. More informations on instancie.

Throws:

PogException

instancie

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

Replace this with the parameter in the modifies clause.

Parameters:

b - expression on which the metohd is called.

Throws:

PogException

renameParam

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

Renames the parameter in the modifies clause.

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)

linkStatements

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

Links the content of the clause.

Parameters:

f - context for link

Returns:

the calculated link informations

Throws:

Jml2bException

processIdent

public abstract void processIdent()

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.

See Also:

jml2b.pog.IdentifierResolver#bIdents

toJava

public abstract java.lang.String toJava(int indent)

Converts the clause into a string.

Returns:

the original string reconstructed associated with this clause

modifies

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

Returns the proof modified in manner to take into account the modifies clause of a called method.

Parameters:

s - current proof

Returns:

the proof where modified variable have been replaced with new variable and where properties concerning those new variables have been added in hypothesis.

Throws:

PogException

modifiesLemmas

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

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

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 abstract void addDepends(IJml2bConfiguration config,
                                Class c)
                         throws PogException

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

Parameters:

c - The defining class of the depends clauses

Throws:

PogException

completeModifiesWithFields

public abstract ModifiesClause completeModifiesWithFields(ModifiesList l)

Parameters:

l -

Returns:

ModifiesClause

setParsedItem

public abstract void setParsedItem(ParsedItem pi)

getFields

public java.util.Collection getFields()