jml2b.structure.statement
Class Statement

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

All Implemented Interfaces:

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

Direct Known Subclasses:

Expression, StAssert, StBlock, StControlFlowBreak, StIf, StImplementsLabel, StLabel, StLoops, StSequence, StSkip, StSpecBlock, StSwitch, StTry, StVarDecl

public abstract class Statement

extends ParsedItem

implements jml.JmlDeclParserTokenTypes, MyToken, Linkable, IFormToken, TypeCheckable

This class defines a Java statement. A statement is either:

• an expression
• an assertion
• a block
• a control flow break (return, break, continue or throw)
• an if
• an implements label
• a label
• a loop (do while, while do or for)
• a sequence
• a skip
• a specified block
• a switch
• a try catch finally
• a variable declaration.

Author:

L. Burdy

See Also:

Serialized Form

Field Summary

static AClass	arithmeticException The Class ArithmeticException
static AClass	arrayIndexOutOfBoundsException The Class ArrayIndexOutOfBoundsException
static AClass	arrayStoreException The Class ArrayStoreException
static AClass	classCastException The Class ClassCastException
static AClass	negativeArraySizeException The Class NegativeArraySizeException
static AClass	nullPointerException The Class NullPointerException

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

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

java.lang.Object	clone()
abstract void	collectCalledMethod(java.util.Vector calledMethod)
static Statement	createS(JmlFile jf, antlr.collections.AST tree) Creates a statement from an AST.
abstract java.lang.String	emit()
Proofs	ensures(IJml2bConfiguration config, Proofs phi1, ExceptionalBehaviourStack phi7)
Proofs	ensures(IJml2bConfiguration config, Theorem phi1, ExceptionalBehaviourStack phi7, java.util.Vector signature) Returns the proofs resulting where the WP calculus apply on this statement.
Statement	firstStatement() Returns the first statement in a sequence.
static java.lang.String	fresh() Returns a fresh temporary variable.
static java.lang.String	freshObject() Returns a fresh new object variable.
static java.lang.String	freshResult(java.lang.String m) Returns a fresh returned from method call variable.
abstract void	getAssert(java.util.Vector asser)
abstract void	getLoop(java.util.Vector loops)
StLoops	getLoopAtLine(int line)
abstract void	getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
abstract void	getSpecBlock(java.util.Vector blocks)
static void	initFresh() Initialize global variables for name generation.
abstract Statement	jmlNormalize(IJml2bConfiguration config, Class definingClass) Collects all the indentifier of the statement to give them an index in the identifer array.
void	link(IJml2bConfiguration config, LinkContext f)
abstract LinkInfo	linkStatement(IJml2bConfiguration config, LinkContext f) Links the statement.
int	linkStatements(IJml2bConfiguration config, LinkContext f)
abstract antlr.collections.AST	parse(antlr.collections.AST tree) Parses an AST tree in order to instanciate the statement fields.
Statement	tail() Returns the tail statement in a sequence considered as a list.
abstract Proofs	wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour) Returns the proofs resulting where the WP calculus apply on this statement.

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

Field Detail

nullPointerException

public static AClass nullPointerException

The Class NullPointerException

See Also:

jml2b.pog.Pog#pog(JmlFile, IJml2bConfiguration)

arrayIndexOutOfBoundsException

public static AClass arrayIndexOutOfBoundsException

The Class ArrayIndexOutOfBoundsException

See Also:

jml2b.pog.Pog#pog(JmlFile, IJml2bConfiguration)

arithmeticException

public static AClass arithmeticException

The Class ArithmeticException

See Also:

jml2b.pog.Pog#pog(JmlFile, IJml2bConfiguration)

negativeArraySizeException

public static AClass negativeArraySizeException

The Class NegativeArraySizeException

See Also:

jml2b.pog.Pog#pog(JmlFile, IJml2bConfiguration)

classCastException

public static AClass classCastException

The Class ClassCastException

See Also:

jml2b.pog.Pog#pog(JmlFile, IJml2bConfiguration)

arrayStoreException

public static AClass arrayStoreException

The Class ArrayStoreException

See Also:

jml2b.pog.Pog#pog(JmlFile, IJml2bConfiguration)

Method Detail

fresh

public static java.lang.String fresh()

Returns a fresh temporary variable.

Returns:

a tempory variable "Txxx"

freshObject

public static java.lang.String freshObject()

Returns a fresh new object variable.

Returns:

a new object variable "newObject_xxx"

freshResult

public static java.lang.String freshResult(java.lang.String m)

Returns a fresh returned from method call variable.

Returns:

a returned from method call variable "Result_xxx"

initFresh

public static void initFresh()

Initialize global variables for name generation.

createS

public static Statement createS(JmlFile jf,
                                antlr.collections.AST tree)
                         throws Jml2bException

Creates a statement from an AST.

Parameters:

jf - JML file where is located this statement

tree - AST node corresponding to this statement

Returns:

tne newly created statement to be instanciated by the parse methods.

Throws:

Jml2bException

clone

public java.lang.Object clone()

ensures

public final Proofs ensures(IJml2bConfiguration config,
                            Theorem phi1,
                            ExceptionalBehaviourStack phi7,
                            java.util.Vector signature)
                     throws Jml2bException,
                            PogException

Returns the proofs resulting where the WP calculus apply on this statement. The statement corresponds to a method body.

Parameters:

phi1 - The normal behaviour to prove if the statement terminates normally or abruptly on a return.

phi7 - The exceptional behaviour to prove if the statement terminates abruply on an exception.

signature - The signature of the method.

Returns:

the proof obligations.

Throws:

PogException - if an error occurs during the PO generation.

Jml2bException

ensures

public final Proofs ensures(IJml2bConfiguration config,
                            Proofs phi1,
                            ExceptionalBehaviourStack phi7)
                     throws Jml2bException,
                            PogException

Throws:

Jml2bException

PogException

link

public final void link(IJml2bConfiguration config,
                       LinkContext f)
                throws Jml2bException

Specified by:

link in interface Linkable

Throws:

Jml2bException

See Also:

Linkable.link(IJml2bConfiguration, LinkContext)

linkStatements

public final int linkStatements(IJml2bConfiguration config,
                                LinkContext f)
                         throws Jml2bException

Specified by:

linkStatements in interface Linkable

Throws:

Jml2bException

See Also:

Linkable.linkStatements(IJml2bConfiguration, LinkContext)

firstStatement

public Statement firstStatement()

Returns the first statement in a sequence. If the statement is not a sequence, return it.

Returns:

this

See Also:

StSequence.firstStatement()

tail

public Statement tail()

Returns the tail statement in a sequence considered as a list. If the statement is not a sequence, return it.

Returns:

this

See Also:

StSequence.tail()

parse

public abstract antlr.collections.AST parse(antlr.collections.AST tree)
                                     throws Jml2bException

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

Parameters:

tree - AST tree containing the statement

Throws:

Jml2bException - when a parse error occurs.

linkStatement

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

Links the statement.

Returns:

the link info resulting from the link

Throws:

Jml2bException

jmlNormalize

public abstract Statement jmlNormalize(IJml2bConfiguration config,
                                       Class definingClass)
                                throws PogException

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. Instancie the statement. More informations on instancie.

Parameters:

definingClass - The class where this statement is defined

Returns:

the normalized statement

Throws:

PogException

See Also:

jml2b.pog.IdentifierResolver#bIdents

wp

public abstract Proofs wp(IJml2bConfiguration config,
                          Proofs normalBehaviour,
                          Proofs finishOnReturn,
                          LabeledProofsVector finishOnBreakLab,
                          LabeledProofsVector finishOnContinueLab,
                          ExceptionalBehaviourStack exceptionalBehaviour)
                   throws Jml2bException,
                          PogException

Returns the proofs resulting where the WP calculus apply on this statement.

Parameters:

normalBehaviour - theorems to ensure if the statement terminates normally

finishOnReturn - theorems to ensure if the statement terminates abruptly on a return

finishOnBreakLab - labelled theorems to ensure if the statement terminates abruptly on a break

finishOnContinueLab - labelled theorems to ensure if the statement terminates abruptly on a continue

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

Returns:

the proofs obligation resulting from the WP calculus

Throws:

PogException

Jml2bException

emit

public abstract java.lang.String emit()

getLoopAtLine

public StLoops getLoopAtLine(int line)

Parameters:

line -

Returns:

getPrecondition

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

Throws:

Jml2bException

PogException

collectCalledMethod

public abstract void collectCalledMethod(java.util.Vector calledMethod)

getAssert

public abstract void getAssert(java.util.Vector asser)

getSpecBlock

public abstract void getSpecBlock(java.util.Vector blocks)

getLoop

public abstract void getLoop(java.util.Vector loops)