jml2b.structure.statement
Class BinaryExp

java.lang.Object
  extended byjml2b.util.Profiler
      extended byjml2b.structure.java.ParsedItem
          extended byjml2b.structure.statement.Statement
              extended byjml2b.structure.statement.Expression
                  extended byjml2b.structure.statement.BinaryExp
All Implemented Interfaces:
IFormToken, jml.JmlDeclParserTokenTypes, JmlExpression, Linkable, MyToken, java.io.Serializable, TypeCheckable

public class BinaryExp
extends Expression

This class implements binary expressions. Java binary expressions can be:

Jml binary expressions can be:

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
BinaryExp(int nodeType, Expression left, java.lang.String nodeText, Expression right)
          Constructs a quantified expression form another one
 
Method Summary
 java.lang.Object clone()
           
 void collectCalledMethod(java.util.Vector calledMethod)
           
 boolean equals(Expression e)
          Returns whether two expressions are equal.
 Expression getLeft()
          Returns the left expression.
 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)
           
 Expression getRight()
          Returns the right expression.
 int getValue()
          Return the value associated to a constant expression.
 JmlExpression instancie()
          Instancie the expression.
 JmlExpression instancie(Expression b)
          Replaces this with the parameter in the expression.
 boolean isConstant()
          Returns whether this expression is a constant.
 void isModifiersCompatible(Modifiers modifiers)
          Tests whether the expression contains fields that have modifiers 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()
          Collects all the indentifier of the statement to give them an index in the identifer 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 normalProof, ExceptionalBehaviourStack exceptionalProof)
          Returns the proofs resulting where the WP calculus apply on this 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

BinaryExp

public BinaryExp(int nodeType,
                 Expression left,
                 java.lang.String nodeText,
                 Expression right)
Constructs a quantified expression form another one

Parameters:
nodeType - The node type
nodeText - The node text
left - The left expression
right - The right 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)
                            throws Jml2bException
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
Throws:
Jml2bException - when a parse error occurs.

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()
Description copied from class: Expression
Collects all the indentifier of the statement 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 Expression
See Also:
jml2b.pog.IdentifierResolver#bIdents

isModifiersCompatible

public void isModifiersCompatible(Modifiers modifiers)
                           throws LinkException
Description copied from class: Expression
Tests whether the expression contains fields that have modifiers 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()
Description copied from interface: JmlExpression
Instancie the expression. More informations on instancie.

Returns:
the instanciated expression

instancie

public JmlExpression instancie(Expression b)
Description copied from class: Expression
Replaces this with the parameter in the expression.

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

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

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 normalProof,
                 ExceptionalBehaviourStack exceptionalProof)
          throws Jml2bException,
                 PogException
Description copied from class: Expression
Returns the proofs resulting where the WP calculus apply on this expression. The calculus is only applied on Java expression.

Specified by:
wp in class Expression
Parameters:
config - the current configuration of the generator
normalProof - theorems to ensure if the expression evaluation terminates normally
exceptionalProof - 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

getLeft

public Expression getLeft()
Returns the left expression.

Returns:
left

getRight

public Expression getRight()
Returns the right expression.

Returns:
right

getPrecondition

public void getPrecondition(IJml2bConfiguration config,
                            ModifiableSet modifies,
                            java.util.Vector req,
                            java.util.Vector ens)
                     throws Jml2bException,
                            PogException
Specified by:
getPrecondition in class Statement
Throws:
Jml2bException
PogException

collectCalledMethod

public void collectCalledMethod(java.util.Vector calledMethod)
Specified by:
collectCalledMethod in class Statement