Uses of Class
jml2b.structure.statement.Expression

Packages that use Expression

jack.plugin
jml2b
jml2b.formula	Provides the classes necessary to create and manage formulas.
jml2b.pog.lemma
jml2b.pog.util
jml2b.structure
jml2b.structure.bytecode
jml2b.structure.java
jml2b.structure.jml	Provides the classes necessary to create and manage jml clauses such that depends, represents, specification cases, modifies and exsures.
jml2b.structure.statement	Provides the classes necessary to create and manage java and jml statements and expressions.
jml2b.util

Uses of Expression in jack.plugin

Methods in jack.plugin that return Expression

Expression	JackJml2bConfiguration.getDefaultRequires()
Expression	JackJml2bConfiguration.getDefaultEnsures()

Uses of Expression in jml2b

Methods in jml2b that return Expression

Expression	IJml2bConfiguration.getDefaultRequires() Returns the default requires clause
Expression	IJml2bConfiguration.getDefaultEnsures() Returns the default ensures clause
Expression	Jml2bConfig.getDefaultRequires()
Expression	Jml2bConfig.getDefaultEnsures()

Uses of Expression in jml2b.formula

Methods in jml2b.formula that return Expression

Expression

TerminalForm.toExp()

Uses of Expression in jml2b.pog.lemma

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

void

Proofs.finalize(IJml2bConfiguration config, Formula param, Expression invStaticFinalFields, Formula hyp, Formula req, java.lang.String name, ColoredInfo b, ColoredInfo method) Finalize the proof obligations by adding the parameters typing in hypothesis adding the invariant coming from the final static field initialization in hypothesis adding the invariant in hypothesis adding the requires of the current method in hypothesis assigning a name

Proofs

Proofs.param(IJml2bConfiguration config, java.util.Vector signature, Expression param, ExceptionalBehaviourStack exceptionalBehaviour) Renames the formal parameter of a called method by the calling parameters.

Constructors in jml2b.pog.lemma with parameters of type Expression

ExsuresLemma(IJml2bConfiguration config, Exsures ex, Expression b, GoalOrigin origin)
Constructs an exsures lemma from an exsures clause

SimpleLemma(IJml2bConfiguration config, Expression f, GoalOrigin origin)
Constructs a lemma from an expression.

Theorem(IJml2bConfiguration config, java.util.Enumeration e, Expression b, GoalOrigin origin)
Construct a theorem from an enumeration of Exsures.

VariantLemma(IJml2bConfiguration config, Expression f)

Uses of Expression in jml2b.pog.util

Constructors in jml2b.pog.util with parameters of type Expression

TemporaryField(ParsedItem pi, Modifiers m, Type t, java.lang.String n, Expression a)
Constructs a temporary field from a field with a new name.

Uses of Expression in jml2b.structure

Methods in jml2b.structure that return Expression

abstract Expression	AField.getAssign()
abstract Expression	AMethod.getNormalizedRequires(IJml2bConfiguration config)
abstract Expression	AMethod.getNormalizedEnsures(IJml2bConfiguration config)
abstract Expression	AMethod.getRequires()

Uses of Expression in jml2b.structure.bytecode

Methods in jml2b.structure.bytecode that return Expression

Expression	ClassField.getAssign()
Expression	ClassFile.getStaticFinalFieldsInvariants()
Expression	ClassMethod.getNormalizedRequires(IJml2bConfiguration config)
Expression	ClassMethod.getNormalizedEnsures(IJml2bConfiguration config)
Expression	ClassMethod.getRequires()

Uses of Expression in jml2b.structure.java

Methods in jml2b.structure.java that return Expression

abstract Expression	AClass.getStaticFinalFieldsInvariants()
Expression	Class.getStaticFinalFieldsInvariants()
Expression	Field.getAssign() Returns the Expression object corresponding to the assign clause of this field The assign clause of a field corresponds to its initialisation, when an initialisation is given during the declaration of the field.
Expression	Field.getDefaultInitialiser()
Expression	Invariant.getInvariant() Returns the expression corresponding to the invariant.
Expression	Method.getNormalizedRequires(IJml2bConfiguration config)
Expression	Method.getNormalizedEnsures(IJml2bConfiguration config)
Expression	Method.getExsuresAsExpression(IJml2bConfiguration config)
Expression	Method.getEnsuresAsExpression(IJml2bConfiguration config)
Expression	Method.getRequires()

Methods in jml2b.structure.java with parameters of type Expression

void	Field.setAssign(Expression a) Sets the Expression object corresponding to the assign clause of the field.
void	Method.addAnnotation(IJml2bConfiguration config, Expression req, SpecCase sc)
boolean	Method.addAnnotation(IJml2bConfiguration config, Expression req, Expression ens, ModifiesClause mod)
boolean	Method.addComputedRequires(IJml2bConfiguration config, Expression r)
void	Method.setRequires(Expression expression)

Constructors in jml2b.structure.java with parameters of type Expression

Field(ParsedItem pi, Modifiers m, Type t, java.lang.String n, Expression a)

Uses of Expression in jml2b.structure.jml

Methods in jml2b.structure.jml that return Expression

Expression	Exsures.getExpression() Returns the property ensured by this exsures clause.
Expression	ModifiesDot.getLeftE()
Expression	Represents.getGluingInvariant() Returns the gluing invariant.
Expression	SpecArrayDotDot.getE1()
Expression	SpecArrayDotDot.getE2()
Expression	SpecArrayExpr.getE()
Expression	SpecCase.getNormalizedEnsures() Returns the ensures clause guarded by the requires clause
Expression	SpecCase.getExsuresAsExpression()
Expression	SpecCase.getEnsures() Returns the content of the ensures clause.
Expression	SpecCase.getRequires() Returns the content of the requires clause.

Methods in jml2b.structure.jml with parameters of type Expression

JmlExpression	JmlExpression.instancie(Expression b) Replaces this with the parameter in the expression.
abstract void	ModifiesClause.instancie(Expression b, IJml2bConfiguration config) Replace this with the parameter in the modifies clause.
void	ModifiesEverything.instancie(Expression b, IJml2bConfiguration config)
void	ModifiesList.instancie(Expression b, IJml2bConfiguration config)
void	ModifiesNothing.instancie(Expression b, IJml2bConfiguration config)
JmlExpression	Represents.instancie(Expression b)
void	SpecCase.completeSpecCase(IJml2bConfiguration config, Expression req, java.util.Vector labels, Modifiers mods, Modifiers methodMods, int type) Completes the modifies, if no modifies were declared, the modifies becomes a modifies \everything
boolean	SpecCase.addAnnotation(IJml2bConfiguration config, Expression ens, ModifiesClause mod)
void	SpecCase.setEnsures(Expression expression)
void	SpecCase.setRequires(Expression expression)

Constructors in jml2b.structure.jml with parameters of type Expression

Exsures(Type t, java.lang.String name, Expression s)
Constructs an exsure clause.

SpecCase(Expression ens, ModifiesClause mod)

Uses of Expression in jml2b.structure.statement

Subclasses of Expression 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	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	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 Expression

Expression	ArrayInitializer.subField(Field f, Field newF)
Expression	ArrayInitializer.subResult(java.lang.String ww)
Expression	BinaryExp.subField(Field f, Field newF)
Expression	BinaryExp.subResult(java.lang.String ww)
Expression	BinaryExp.getLeft() Returns the left expression.
Expression	BinaryExp.getRight() Returns the right expression.
static Expression	Expression.getNull() Returns the expression null.
static Expression	Expression.getFalse() Returns the expression false.
static Expression	Expression.getTrue() Returns the expression true.
static Expression	Expression.getZero() Returns the expression 0.
static Expression	Expression.getFromString(java.lang.String expression)
static Expression	Expression.createE(JmlFile jf, antlr.collections.AST tree) Creates an expression from an AST node.
Expression	Expression.normComma(Expression t) Normalized comma expression (a,b),c in a,(b,c).
Expression	Expression.renameParam(Parameters signature, Parameters newSignature) Renames the fields belonging to the parameter list with new names.
abstract Expression	Expression.subField(Field f, Field newF)
abstract Expression	Expression.subResult(java.lang.String ww)
Expression	Expression.addInConjonction(Expression req)
Expression	IsSubtypeOfExp.subField(Field f, Field newF)
Expression	IsSubtypeOfExp.subResult(java.lang.String ww)
Expression	IsSubtypeOfExp.getSubType()
Expression	IsSubtypeOfExp.getType()
Expression	MethodCallExp.subField(Field f, Field newF)
Expression	MethodCallExp.subResult(java.lang.String ww)
Expression	MethodCallExp.getLeft() Returns the expression corresponding to the called method.
Expression	MethodCallExp.getRight()
Expression	QuantifiedExp.subField(Field f, Field newF)
Expression	QuantifiedExp.subResult(java.lang.String ww)
Expression	QuantifiedExp.getBody()
Expression	QuestionExp.subField(Field f, Field newF)
Expression	QuestionExp.subResult(java.lang.String ww)
Expression	QuestionExp.getCond()
Expression	QuestionExp.getLeft()
Expression	QuestionExp.getRight()
Expression	StAssert.getExp()
Expression	StLoops.getLoop_invariant() Returns the loop invariant.
Expression	StLoops.getLoop_variant()
Expression	TTypeExp.subField(Field f, Field newF)
Expression	TTypeExp.subResult(java.lang.String ww)
Expression	TerminalExp.subField(Field f, Field newF)
Expression	TerminalExp.subResult(java.lang.String ww)
Expression	UnaryExp.subField(Field f, Field newF)
Expression	UnaryExp.subResult(java.lang.String ww)
Expression	UnaryExp.getExp()
Expression	WithTypeExp.subField(Field f, Field newF)
Expression	WithTypeExp.subResult(java.lang.String ww)
Expression	WithTypeExp.getExp()

Methods in jml2b.structure.statement with parameters of type Expression

boolean	ArrayInitializer.equals(Expression e)
JmlExpression	ArrayInitializer.instancie(Expression b)
boolean	BinaryExp.equals(Expression e)
JmlExpression	BinaryExp.instancie(Expression b)
static BinaryExp	Expression.and(Expression s1, Expression s2) Returns the conjonction of two expressions.
Expression	Expression.normComma(Expression t) Normalized comma expression (a,b),c in a,(b,c).
abstract boolean	Expression.equals(Expression e) Returns whether two expressions are equal.
abstract JmlExpression	Expression.instancie(Expression b) Replaces this with the parameter in the expression.
Expression	Expression.addInConjonction(Expression req)
boolean	IsSubtypeOfExp.equals(Expression e)
JmlExpression	IsSubtypeOfExp.instancie(Expression b)
boolean	MethodCallExp.equals(Expression e)
JmlExpression	MethodCallExp.instancie(Expression b)
boolean	QuantifiedExp.equals(Expression e)
JmlExpression	QuantifiedExp.instancie(Expression b)
boolean	QuestionExp.equals(Expression e)
JmlExpression	QuestionExp.instancie(Expression b)
boolean	TTypeExp.equals(Expression e)
JmlExpression	TTypeExp.instancie(Expression b)
boolean	TerminalExp.equals(Expression e)
JmlExpression	TerminalExp.instancie(Expression b) If the current expression is LITERAL_this, return b else return this.
boolean	UnaryExp.equals(Expression e)
JmlExpression	UnaryExp.instancie(Expression b)
boolean	WithTypeExp.equals(Expression e)
JmlExpression	WithTypeExp.instancie(Expression b)

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

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

MethodCallExp(int nodeType, Expression left, java.lang.String nodeText, Expression right)
Constructs a method call expression form another one

QuantifiedExp(int nodeType, java.lang.String nodeText, QuantifiedVar vars, Expression body)
Constructs a quantified expression form another one

UnaryExp(int nodeType, java.lang.String nodeText, Expression exp)
Constructs an unary expression form another unary expression.

Uses of Expression in jml2b.util

Methods in jml2b.util that return Expression

static Expression

StatementUtils.andEnumeration(java.util.Enumeration e) Return an expression corresponding to the "and" of all the expression enumerated.