jml2b.structure.java
Class Method

java.lang.Object
  jml2b.util.Profiler
      jml2b.structure.java.ParsedItem
          jml2b.structure.java.NamedNode
              jml2b.structure.java.Declaration
                  jml2b.structure.AMethod
                      jml2b.structure.java.Method

All Implemented Interfaces:

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

Direct Known Subclasses:

Constructor

public class Method

extends AMethod

implements java.io.Serializable, IModifiesField, TypeCheckable

Author:

L. Burdy, A. Requet

See Also:

Serialized Form

Field Summary

Proofs	lemmas
Proofs	wellDefinednessLemmas

Fields inherited from class jml2b.structure.java.NamedNode

garbage, nameIndex

Fields inherited from interface jml2b.link.Linkable

STATE_LINKED, STATE_LINKED_STATEMENTS, STATE_LINKED_TYPE_CHECKED, STATE_UNLINKED

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

Constructor Summary

Method()

Method(JmlFile jf, antlr.collections.AST tree, Modifiers m, Class defining)

Method(ParsedItem pi, Modifiers m, Class defining)

Method Summary

boolean	addAnnotation(IJml2bConfiguration config, Expression req, Expression ens, ModifiesClause mod)
void	addAnnotation(IJml2bConfiguration config, Expression req, SpecCase sc)
boolean	addComputedModifies(IJml2bConfiguration config, ModifiesList ml)
boolean	addComputedRequires(IJml2bConfiguration config, Expression r)
java.util.Collection	annotate(IJml2bConfiguration config)
java.lang.String	emitSpecCase(IJml2bConfiguration config)
boolean	exactMatch(java.util.Vector param_types) Returns true if the given method has exactly the same signature as the given vector of types.
java.util.HashSet	getAnnotatedModifies()
java.util.Vector	getAnnotatedPostcondition()
java.util.Vector	getAnnotatedPrecondition()
Statement	getBody(IJml2bConfiguration config)
java.util.Enumeration	getCalledMethods()
java.util.Vector	getClonedSpecCases(ParsedItem pi)
ModifiesClause	getDefaultLoopModifies()
Expression	getEnsuresAsExpression(IJml2bConfiguration config)
Expression	getExsuresAsExpression(IJml2bConfiguration config)
int	getFirstLine()
java.lang.String	getInfo()
java.lang.String	getInfo(java.lang.String ret)
Proofs	getLemmas()
StLoops	getLoopAtLine(int line)
java.lang.String	getName()
Expression	getNormalizedEnsures(IJml2bConfiguration config)
Expression	getNormalizedRequires(IJml2bConfiguration config)
IAParameters	getParams()
java.lang.String	getParamsString()
java.lang.String	getPmiName()
Expression	getRequires()
Type	getReturnType()
java.lang.String	getSignature()
java.util.Enumeration	getSpecCases(IJml2bConfiguration config) Returns the specCases elements.
java.util.Vector	getSpecCasesV(IJml2bConfiguration config) Returns the specCases.
int	getSpecType()
AMethod	getSuperMethod()
Proofs	getWellDefinednessLemmas()
boolean	hasNoCode()
boolean	isAnnotated()
boolean	isConstructor()
boolean	isStatic()
void	link(IJml2bConfiguration config, LinkContext f)
int	linkStatements(IJml2bConfiguration config, LinkContext f)
boolean	matchWith(IJml2bConfiguration config, Method m)
int	nbPo()
int	nbPoChecked()
int	nbPoProved()
int	nbPoProved(java.lang.String prover)
antlr.collections.AST	parse(JmlFile jmlFile, antlr.collections.AST a) Parses the content of the declaration.
void	save(IJml2bConfiguration config, JpoOutputStream s, JmlFile jf) .jpo file
void	setPmiName(java.lang.String n)
void	setRequires(Expression expression)
void	setReturnType(Type returnType)
void	setSpecCases(java.util.Vector vector)
java.lang.String	toString()
Type	typeCheck(IJml2bConfiguration config, LinkContext f)

Methods inherited from class jml2b.structure.AMethod

getNameForModifies

Methods inherited from class jml2b.structure.java.Declaration

getDefiningClass, getModifiers, isVisibleFrom, setDefiningClass

Methods inherited from class jml2b.structure.java.NamedNode

clearName, getBName, hasBName, newName

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

Methods inherited from interface jml2b.formula.IModifiesField

getNameForModifies

Field Detail

lemmas

public transient Proofs lemmas

wellDefinednessLemmas

public transient Proofs wellDefinednessLemmas

Constructor Detail

Method

public Method()

Method

public Method(JmlFile jf,
              antlr.collections.AST tree,
              Modifiers m,
              Class defining)
       throws Jml2bException

Method

public Method(ParsedItem pi,
              Modifiers m,
              Class defining)
       throws Jml2bException

Method Detail

getParams

public IAParameters getParams()

Specified by:

getParams in class AMethod

getParamsString

public java.lang.String getParamsString()

getBody

public Statement getBody(IJml2bConfiguration config)
                  throws Jml2bException,
                         PogException

Throws:

Jml2bException

PogException

hasNoCode

public boolean hasNoCode()

parse

public antlr.collections.AST parse(JmlFile jmlFile,
                                   antlr.collections.AST a)
                            throws Jml2bException

Description copied from class: Declaration

Parses the content of the declaration.

Specified by:

parse in class Declaration

Parameters:

jmlFile - the file the class that defines the declaration is loaded from.

a - the AST containing the declaration tree.

Returns:

AST the AST following the declaration.

Throws:

Jml2bException - in case of parse error.

link

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

Specified by:

link in interface Linkable

Throws:

Jml2bException

linkStatements

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

Specified by:

linkStatements in interface Linkable

Throws:

Jml2bException

typeCheck

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

Specified by:

typeCheck in interface TypeCheckable

Throws:

Jml2bException

getReturnType

public Type getReturnType()

Specified by:

getReturnType in class AMethod

getName

public java.lang.String getName()

Specified by:

getName in class AMethod

Returns:

isConstructor

public boolean isConstructor()

Specified by:

isConstructor in class AMethod

isStatic

public boolean isStatic()

toString

public java.lang.String toString()

getPmiName

public java.lang.String getPmiName()

setPmiName

public void setPmiName(java.lang.String n)

nbPoChecked

public int nbPoChecked()

Returns:

nbPo

public int nbPo()

nbPoProved

public int nbPoProved(java.lang.String prover)

nbPoProved

public int nbPoProved()

getSuperMethod

public AMethod getSuperMethod()

getNormalizedRequires

public Expression getNormalizedRequires(IJml2bConfiguration config)
                                 throws Jml2bException,
                                        PogException

Specified by:

getNormalizedRequires in class AMethod

Throws:

Jml2bException

PogException

getNormalizedEnsures

public Expression getNormalizedEnsures(IJml2bConfiguration config)
                                throws Jml2bException,
                                       PogException

Specified by:

getNormalizedEnsures in class AMethod

Throws:

Jml2bException

PogException

getExsuresAsExpression

public Expression getExsuresAsExpression(IJml2bConfiguration config)
                                  throws Jml2bException,
                                         PogException

Throws:

Jml2bException

PogException

getEnsuresAsExpression

public Expression getEnsuresAsExpression(IJml2bConfiguration config)
                                  throws Jml2bException,
                                         PogException

Throws:

Jml2bException

PogException

getInfo

public java.lang.String getInfo()

Specified by:

getInfo in class AMethod

getInfo

public java.lang.String getInfo(java.lang.String ret)

Specified by:

getInfo in class AMethod

getSpecCases

public java.util.Enumeration getSpecCases(IJml2bConfiguration config)
                                   throws Jml2bException,
                                          PogException

Returns the specCases elements.

Specified by:

getSpecCases in class AMethod

Returns:

Enumeration

Throws:

Jml2bException

PogException

getSpecCasesV

public java.util.Vector getSpecCasesV(IJml2bConfiguration config)
                               throws Jml2bException,
                                      PogException

Returns the specCases.

Returns:

Vector

Throws:

Jml2bException

PogException

emitSpecCase

public java.lang.String emitSpecCase(IJml2bConfiguration config)

getClonedSpecCases

public java.util.Vector getClonedSpecCases(ParsedItem pi)

Specified by:

getClonedSpecCases in class AMethod

getLoopAtLine

public StLoops getLoopAtLine(int line)

Parameters:

line -

Returns:

getLemmas

public Proofs getLemmas()

Returns:

getWellDefinednessLemmas

public Proofs getWellDefinednessLemmas()

Returns:

matchWith

public boolean matchWith(IJml2bConfiguration config,
                         Method m)
                  throws Jml2bException

Throws:

Jml2bException

addAnnotation

public void addAnnotation(IJml2bConfiguration config,
                          Expression req,
                          SpecCase sc)
                   throws Jml2bException,
                          PogException

Throws:

Jml2bException

PogException

addAnnotation

public boolean addAnnotation(IJml2bConfiguration config,
                             Expression req,
                             Expression ens,
                             ModifiesClause mod)
                      throws Jml2bException,
                             PogException

Throws:

Jml2bException

PogException

getFirstLine

public int getFirstLine()

Returns:

getRequires

public Expression getRequires()

Specified by:

getRequires in class AMethod

Returns:

annotate

public java.util.Collection annotate(IJml2bConfiguration config)
                              throws Jml2bException,
                                     PogException

Throws:

Jml2bException

PogException

addComputedModifies

public boolean addComputedModifies(IJml2bConfiguration config,
                                   ModifiesList ml)
                            throws Jml2bException,
                                   PogException

Throws:

Jml2bException

PogException

addComputedRequires

public boolean addComputedRequires(IJml2bConfiguration config,
                                   Expression r)
                            throws Jml2bException,
                                   PogException

Throws:

Jml2bException

PogException

isAnnotated

public boolean isAnnotated()

getAnnotatedPrecondition

public java.util.Vector getAnnotatedPrecondition()

getAnnotatedModifies

public java.util.HashSet getAnnotatedModifies()

getAnnotatedPostcondition

public java.util.Vector getAnnotatedPostcondition()

getSpecType

public int getSpecType()

Returns:

getDefaultLoopModifies

public ModifiesClause getDefaultLoopModifies()

Returns:

setRequires

public void setRequires(Expression expression)

Parameters:

expression -

setSpecCases

public void setSpecCases(java.util.Vector vector)

Parameters:

vector -

getCalledMethods

public java.util.Enumeration getCalledMethods()

Returns:

getSignature

public java.lang.String getSignature()

Specified by:

getSignature in class AMethod

save

public void save(IJml2bConfiguration config,
                 JpoOutputStream s,
                 JmlFile jf)
          throws java.io.IOException

.jpo file

Throws:

java.io.IOException

setReturnType

public void setReturnType(Type returnType)

exactMatch

public boolean exactMatch(java.util.Vector param_types)

Returns true if the given method has exactly the same signature as the given vector of types.

Specified by:

exactMatch in class AMethod

Parameters:

param_types - a vector of Type elements corresponding to the wanted signature.

Returns:

boolean true if the signature of the candidate method is the same as the param_type vector.