Uses of Class
jml2b.structure.statement.Statement

Packages that use Statement

jml2b.pog.lemma
jml2b.pog.proofobligation
jml2b.structure.java
jml2b.structure.statement	Provides the classes necessary to create and manage java and jml statements and expressions.

Uses of Statement in jml2b.pog.lemma

Methods in jml2b.pog.lemma with parameters of type Statement

ExceptionalBehaviourStack	ExceptionalBehaviourStack.finallyOnExceptionalBehaviour(IJml2bConfiguration config, Statement body, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour) Calculate the ExceptionalProofs stack resulting from the application of the body on the current stack (used to proceed a finally).
ExceptionalProofs	ExceptionalProofs.finallyOnExceptionalBehaviour(IJml2bConfiguration config, Statement body, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour) Calculate the ExceptionalProofs stack resulting from the application of the body on the current stack (used to proceed a finally).
LabeledProofsVector	LabeledProofsVector.finallyLab(IJml2bConfiguration config, Statement body, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour) Applies a WP calculus on all the labeled proofs of the set.

Uses of Statement in jml2b.pog.proofobligation

Constructors in jml2b.pog.proofobligation with parameters of type Statement

ConstructorPO(Class c, java.lang.String s, Method m, Formula h1, Formula h2, ColoredInfo box, Statement b, Theorem p1, Theorem p7)
Constructs a proof obligation

MethodPO(Class c, Method m, Formula h1, Formula h2, ColoredInfo box, Statement b, Theorem p1, Theorem p7)
Constructs a proof obligation

StaticInitializationPO(Class c, Statement b, Theorem p1, Theorem p7)
Constructs a proof obligation

Uses of Statement in jml2b.structure.java

Methods in jml2b.structure.java that return Statement

Statement

Method.getBody(IJml2bConfiguration config)

Uses of Statement in jml2b.structure.statement

Subclasses of Statement in jml2b.structure.statement

class	ArrayInitializer This class implements an array initializer statement, that is, for instance, { {"car", "house" }, {"dog", "cat", "monkey"} }.
class	BinaryExp This class implements binary expressions.
class	Expression This class defines a Java expression.
class	IsSubtypeOfExp This class implements subtype JML expression, it corresponds to code like a <: b
class	MethodCallExp This class implements a method call expression
class	QuantifiedExp This class implements a quantified expression, that is \forall type var; body or \exists type var; body.
class	QuestionExp This class implements a question expression, that is a ? b :c
class	StAssert
class	StBlock This class implements a block statement
class	StControlFlowBreak This class implements a control flow break statement, that is a throw, a continue, a break or a return.
class	StDoWhile
class	StFor
class	StIf
class	StImplementsLabel This class implements an implements label statement.
class	StLabel
class	StLoops This abstract class implements a loop statement.
class	StSequence This class implements a sequence of two statements.
class	StSkip This class implements a skip statement.
class	StSpecBlock This class implements a specified block.
class	StSwitch This class implements a switch statement
class	StTry This class implements a try catch finally statement or a try catch or a try finally statement.
class	StVarDecl This class implements a set of local field declaration statement
class	TerminalExp This class implements a terminal expression.
class	TTypeExp This class implements expressions corresponding to types.
class	UnaryExp This class implements unary expressions.
class	WithTypeExp This class implements expression with type, that is object and array creation, casting and instanceof.

Methods in jml2b.structure.statement that return Statement

Statement	Expression.jmlNormalize(IJml2bConfiguration config, Class definingClass)
Statement	StAssert.jmlNormalize(IJml2bConfiguration config, Class definingClass)
Statement	StBlock.jmlNormalize(IJml2bConfiguration config, Class definingClass)
Statement	StBlock.firstStatement()
Statement	StBlock.tail()
Statement	StBlock.getBody()
Statement	StControlFlowBreak.jmlNormalize(IJml2bConfiguration config, Class definingClass)
Statement	StDoWhile.jmlNormalize(IJml2bConfiguration config, Class definingClass)
Statement	StFor.jmlNormalize(IJml2bConfiguration config, Class definingClass)
Statement	StFor.getUpdater() Returns the updater statement.
Statement	StIf.jmlNormalize(IJml2bConfiguration config, Class definingClass)
Statement	StImplementsLabel.jmlNormalize(IJml2bConfiguration config, Class definingClass)
Statement	StLabel.jmlNormalize(IJml2bConfiguration config, Class definingClass)
Statement	StLoops.jmlNormalize(IJml2bConfiguration config, Class definingClass)
Statement	StLoops.getBody()
Statement	StSequence.jmlNormalize(IJml2bConfiguration config, Class definingClass)
Statement	StSequence.firstStatement()
Statement	StSequence.tail()
Statement	StSkip.jmlNormalize(IJml2bConfiguration config, Class definingClass)
Statement	StSpecBlock.jmlNormalize(IJml2bConfiguration config, Class definingClass)
Statement	StSwitch.jmlNormalize(IJml2bConfiguration config, Class definingClass)
Statement	StTry.jmlNormalize(IJml2bConfiguration config, Class definingClass)
Statement	StVarDecl.jmlNormalize(IJml2bConfiguration config, Class definingClass)
static Statement	Statement.createS(JmlFile jf, antlr.collections.AST tree) Creates a statement from an AST.
Statement	Statement.firstStatement() Returns the first statement in a sequence.
Statement	Statement.tail() Returns the tail statement in a sequence considered as a list.
abstract Statement	Statement.jmlNormalize(IJml2bConfiguration config, Class definingClass) Collects all the indentifier of the statement to give them an index in the identifer array.

Constructors in jml2b.structure.statement with parameters of type Statement

StSequence(ParsedItem pi, Statement left, Statement right)
Constructs a sequence from another one.