jml2b.structure.statement
Class StSpecBlock

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

All Implemented Interfaces:

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

public class StSpecBlock

extends Statement

implements IModifiesField

This class implements a specified block. It corresponds to a block prefixed with a JML lightweight specification. This expression has been added to the JML syntax. It allows to cut proof obligation generation process by simulating a method call.

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 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

void	collectCalledMethod(java.util.Vector calledMethod)
java.lang.String	emit()
void	getAssert(java.util.Vector asser)
int	getEndLine()
void	getLoop(java.util.Vector asser)
java.lang.String	getNameForModifies()
void	getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
SpecCase	getSp()
void	getSpecBlock(java.util.Vector asser)
int	getStartLine()
Statement	jmlNormalize(IJml2bConfiguration config, Class definingClass) Collects all the indentifier of the statement to give them an index in the identifer array.
LinkInfo	linkStatement(IJml2bConfiguration config, LinkContext f) Links the statement.
antlr.collections.AST	parse(antlr.collections.AST tree) Parses an AST tree in order to instanciate the statement fields.
Type	typeCheck(IJml2bConfiguration config, LinkContext f)
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.statement.Statement

clone, 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

Method Detail

emit

public java.lang.String emit()

Specified by:

emit in class Statement

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

Specified by:

typeCheck in interface TypeCheckable

Throws:

Jml2bException

jmlNormalize

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

Description copied from class: Statement

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.

Specified by:

jmlNormalize in class Statement

Parameters:

definingClass - The class where this statement is defined

Returns:

the normalized statement

Throws:

PogException

See Also:

jml2b.pog.IdentifierResolver#bIdents

wp

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

Description copied from class: Statement

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

Specified by:

wp in class 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

getNameForModifies

public java.lang.String getNameForModifies()

Specified by:

getNameForModifies in interface IModifiesField

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

getAssert

public void getAssert(java.util.Vector asser)

Specified by:

getAssert in class Statement

getSpecBlock

public void getSpecBlock(java.util.Vector asser)

Specified by:

getSpecBlock in class Statement

getLoop

public void getLoop(java.util.Vector asser)

Specified by:

getLoop in class Statement

getSp

public SpecCase getSp()

Returns:

getEndLine

public int getEndLine()

Returns:

getStartLine

public int getStartLine()

Returns: