jml2b.structure.jml
Class ModifiesEverything

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

All Implemented Interfaces:

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

public class ModifiesEverything

extends ModifiesClause

This class implements a \everything

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

ModifiesEverything()
Constructs an empty modifies clause.

Method Summary

void	addDepends(IJml2bConfiguration config, Class c) Performs no action
java.lang.Object	clone() Clones the object.
ModifiesClause	completeModifiesWithFields(ModifiesList l)
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) Returns the proof modified in manner to take into account the modifies clause of a called method.
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, getFields

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

ModifiesEverything

public ModifiesEverything()

Constructs an empty modifies clause.

Method Detail

clone

public java.lang.Object clone()

Description copied from class: ModifiesClause

Clones the object.

Specified by:

clone in class ModifiesClause

Returns:

the cloned object

instancie

public void instancie(IJml2bConfiguration config)

Description copied from class: ModifiesClause

Instancie the modifies clause. More informations on instancie.

Specified by:

instancie in class ModifiesClause

instancie

public void instancie(Expression b,
                      IJml2bConfiguration config)

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.

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

Throws:

Jml2bException

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:

\everything

modifiesLemmas

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

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:

an empty lemma

renameParam

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

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:

this

See Also:

Proofs#renameParam(Parameters, Vector)

addDepends

public void addDepends(IJml2bConfiguration config,
                       Class c)

Performs no action

Specified by:

addDepends in class ModifiesClause

Parameters:

c - The defining class of the depends clauses

modifies

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

Description copied from class: ModifiesClause

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

Specified by:

modifies in class ModifiesClause

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.

completeModifiesWithFields

public ModifiesClause completeModifiesWithFields(ModifiesList l)

Specified by:

completeModifiesWithFields in class ModifiesClause

Parameters:

l -

Returns:

this

setParsedItem

public void setParsedItem(ParsedItem pi)

Specified by:

setParsedItem in class ModifiesClause