jml2b.structure.jml
Class ModifiesNothing

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

All Implemented Interfaces:

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

public class ModifiesNothing

extends ModifiesClause

This class implements a \nothing modifies clause.

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

ModifiesNothing()
Constructs a \nothing 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 proofs s, till no fields are modified
SimpleLemma	modifiesLemmas(IJml2bConfiguration config, java.util.Vector fields, java.util.Vector nonModifiedFields, Formula[] nonModifiedxxxElements) Returns the lemma corresponding to proof that all the fields and all the array elements have not been modified.
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

ModifiesNothing

public ModifiesNothing()

Constructs a \nothing 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:

\nothing

modifiesLemmas

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

Returns the lemma corresponding to proof that all the fields and all the array elements have not been modified.

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:

The lemmas corresponding to

• f == \old(f) for each static field
• \old(instances) <| f == \old(instances) <| \old(f) for each member field
• old(instances) <| xxxelements == \old(instances) <| \old(xxxelements) for each xxxelements variable.

Throws:

PogException

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)

Returns the proofs s, till no fields are modified

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:

l

setParsedItem

public void setParsedItem(ParsedItem pi)

Specified by:

setParsedItem in class ModifiesClause