jml2b.structure.statement
Class TerminalExp

java.lang.Object
  jml2b.util.Profiler
      jml2b.structure.java.ParsedItem
          jml2b.structure.statement.Statement
              jml2b.structure.statement.Expression
                  jml2b.structure.statement.TerminalExp

All Implemented Interfaces:

IFormToken, jml.JmlDeclParserTokenTypes, JmlExpression, Linkable, MyToken, java.io.Serializable, TypeCheckable

public class TerminalExp

extends Expression

This class implements a terminal expression.

Java terminal expressions can be:

• an identifier
• a Java builtin type
• a float literal
• a char literal
• a integer literal
• a string literal
• false
• true
• null
• this
• super

Jml terminal expressions can be:

• \result

Author:

L. Burdy, A. Requet

See Also:

Serialized Form

Field Summary

Fields inherited from class jml2b.structure.statement.Statement

arithmeticException, arrayIndexOutOfBoundsException, arrayStoreException, classCastException, negativeArraySizeException, nullPointerException

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

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.structure.statement.MyToken

BTRUE, FIRST_TOKEN, METHOD_CALL, NEWARRAY, nodeString, SEQUENCE, SKIP, T_CALLED_OLD, T_FRESH_CALLED_OLD, T_VARIANT_OLD

Fields inherited from interface jml2b.link.Linkable

STATE_LINKED, STATE_LINKED_STATEMENTS, STATE_LINKED_TYPE_CHECKED, STATE_UNLINKED

Constructor Summary

TerminalExp(Identifier ident)
Constructs an expression from a Java identifer.

TerminalExp(Identifier ident, java.lang.String subident)
Constructs an expression from a Java identifer and a postfix string.

TerminalExp(int nodeType, java.lang.String nodeText)
Constructs an expression that is not a Java identifer.

TerminalExp(java.lang.String nodeText, Type t)
Constructs an expression that is an identifier but not a Java identifer.

Method Summary

java.lang.Object	clone()
void	collectCalledMethod(java.util.Vector calledMethod)
boolean	equals(Expression e) Returns whether two expressions are equal.
Identifier	getIdent() Returns the identifier.
java.util.Vector	getParsedItems() Returns the set of parsed items that correspond to this expression
void	getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
int	getValue() Return the value associated to a constant expression.
JmlExpression	instancie() Returns a dot expression this.e where e is the current expression when it is an identifer that corresponds to a non static field or non static method.
JmlExpression	instancie(Expression b) If the current expression is LITERAL_this, return b else return this.
boolean	isConstant() Returns whether this expression is a constant.
void	isModifiersCompatible(Modifiers modifiers) If the expression is an identifier, test if their modifiers are compatible with the invariant modifiers.
LinkInfo	linkStatement(IJml2bConfiguration config, LinkContext f) Links the statement.
void	old() Converts old pragma in called old pragma.
antlr.collections.AST	parse(antlr.collections.AST tree) Parses an AST tree in order to instanciate the statement fields.
void	processIdent() When this terminal expression is an identifier, a name index is assigned and its name is stored in the identifier array.
void	setParsedItem(ParsedItem pi)
Expression	subField(Field f, Field newF)
Expression	subResult(java.lang.String ww)
java.lang.String	toJava(int indent) Displays the expression corresponding to a part of a method specification in a tool tip with the initial Java syntax.
Type	typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	wp(IJml2bConfiguration config, java.lang.String result, Proofs normalBehaviour, ExceptionalBehaviourStack exceptionalBehaviour) Returns the normal behaviour proof where the resulting variable has been substituted with the current expression.

Methods inherited from class jml2b.structure.statement.Expression

addInConjonction, and, createE, emit, exprToForm, getAssert, getFalse, getFromString, getLoop, getNodeText, getNodeType, getNull, getSpecBlock, getStateType, getTrue, getZero, isAnd, isBTrue, isComma, isDot, jmlNormalize, linkMethod, linkParameters, normComma, predToForm, renameParam, setNodeText, setNodeType, setStateType, wp

Methods inherited from class jml2b.structure.statement.Statement

createS, ensures, ensures, firstStatement, fresh, freshObject, freshResult, getLoopAtLine, initFresh, link, linkStatements, tail

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

TerminalExp

public TerminalExp(int nodeType,
                   java.lang.String nodeText)

Constructs an expression that is not a Java identifer.

Parameters:

nodeType - The node type of this expression

nodeText - The string corresponding to this expression

TerminalExp

public TerminalExp(java.lang.String nodeText,
                   Type t)

Constructs an expression that is an identifier but not a Java identifer.

Parameters:

nodeText - The string corresponding to this expression

TerminalExp

public TerminalExp(Identifier ident,
                   java.lang.String subident)

Constructs an expression from a Java identifer and a postfix string.

Parameters:

ident - The identifier corresponding to this expression

subident - The postfix string associated with this expression

TerminalExp

public TerminalExp(Identifier ident)

Constructs an expression from a Java identifer.

Parameters:

ident - The identifier corresponding to this expression

Method Detail

clone

public java.lang.Object clone()

Specified by:

clone in interface JmlExpression

Overrides:

clone in class Statement

equals

public boolean equals(Expression e)

Description copied from class: Expression

Returns whether two expressions are equal.

Specified by:

equals in class Expression

Parameters:

e - The tested expression

Returns:

true if the expression equals the parameter, false otherwise

toJava

public java.lang.String toJava(int indent)

Description copied from class: Expression

Displays the expression corresponding to a part of a method specification in a tool tip with the initial Java syntax.

Specified by:

toJava in class Expression

Returns:

the string corresponding to this expression

parse

public antlr.collections.AST parse(antlr.collections.AST tree)

Description copied from class: Statement

Parses an AST tree in order to instanciate the statement fields.

Specified by:

parse in class Statement

Parameters:

tree - AST tree containing the statement

linkStatement

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

Description copied from class: Statement

Links the statement.

Specified by:

linkStatement in class Statement

Returns:

the link info resulting from the link

Throws:

Jml2bException

typeCheck

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

Throws:

Jml2bException

processIdent

public void processIdent()

When this terminal expression is an identifier, a name index is assigned and its name is stored in the identifier array.

Specified by:

processIdent in class Expression

See Also:

jml2b.pog.IdentifierResolver#bIdents

isModifiersCompatible

public void isModifiersCompatible(Modifiers modifiers)
                           throws LinkException

If the expression is an identifier, test if their modifiers are compatible with the invariant modifiers.

Specified by:

isModifiersCompatible in class Expression

Parameters:

modifiers - The current invariant modifiers

Throws:

LinkException - when the test fails.

instancie

public JmlExpression instancie()

Returns a dot expression this.e where e is the current expression when it is an identifer that corresponds to a non static field or non static method.

Returns:

the instanciated expression

subField

public Expression subField(Field f,
                           Field newF)

Specified by:

subField in class Expression

subResult

public Expression subResult(java.lang.String ww)

Specified by:

subResult in class Expression

instancie

public JmlExpression instancie(Expression b)

If the current expression is LITERAL_this, return b else return this.

Specified by:

instancie in interface JmlExpression

Specified by:

instancie in class Expression

Parameters:

b - expression on which the method where the expression occurs is called.

Returns:

the modified expression

getParsedItems

public java.util.Vector getParsedItems()

Description copied from class: Expression

Returns the set of parsed items that correspond to this expression

Specified by:

getParsedItems in interface JmlExpression

Specified by:

getParsedItems in class Expression

Returns:

the set of parsed item that correspond to the complete expression

setParsedItem

public void setParsedItem(ParsedItem pi)

Specified by:

setParsedItem in class Expression

isConstant

public boolean isConstant()

Description copied from class: Expression

Returns whether this expression is a constant.

Specified by:

isConstant in class Expression

Returns:

true if the expression is a constant, false otherwise

getValue

public int getValue()

Description copied from class: Expression

Return the value associated to a constant expression.

This method should only be called if isConstant returned true.

Overrides:

getValue in class Expression

Returns:

the integer value of the expression

old

public void old()

Description copied from class: Expression

Converts old pragma in called old pragma.

Specified by:

old in class Expression

wp

public Proofs wp(IJml2bConfiguration config,
                 java.lang.String result,
                 Proofs normalBehaviour,
                 ExceptionalBehaviourStack exceptionalBehaviour)
          throws Jml2bException,
                 PogException

Returns the normal behaviour proof where the resulting variable has been substituted with the current expression.

Specified by:

wp in class Expression

Parameters:

config - the current configuration of the generator

normalBehaviour - theorems to ensure if the expression evaluation terminates normally

exceptionalBehaviour - exceptional theorems to ensure if the expression evaluation terminates abruply on an exception

Returns:

the proofs obligation resulting from the WP calculus

Throws:

PogException

Jml2bException

getIdent

public Identifier getIdent()

Returns the identifier.

Returns:

ident

getPrecondition

public void getPrecondition(IJml2bConfiguration config,
                            ModifiableSet modifies,
                            java.util.Vector req,
                            java.util.Vector ens)

Specified by:

getPrecondition in class Statement

collectCalledMethod

public void collectCalledMethod(java.util.Vector calledMethod)

Specified by:

collectCalledMethod in class Statement