Uses of Class
org.jmlspecs.jml4.fspv.theory.TheoryExpression

Packages that use TheoryExpression

org.jmlspecs.jml4.fspv
org.jmlspecs.jml4.fspv.theory

Uses of TheoryExpression in org.jmlspecs.jml4.fspv

Methods in org.jmlspecs.jml4.fspv with parameters of type TheoryExpression

java.lang.Object

SideEffectHandler.accept(TheoryExpression theoryExpression)

Uses of TheoryExpression in org.jmlspecs.jml4.fspv.theory

Subclasses of TheoryExpression in org.jmlspecs.jml4.fspv.theory

class	TheoryAssignmentExpression
class	TheoryBinaryExpression
class	TheoryBlockExpression
class	TheoryInvariantExpression
class	TheoryLiteral
class	TheoryLoopAnnotationsExpression
class	TheoryOldExpression
class	TheoryPostfixExpression
class	TheoryPrefixExpression
class	TheoryQuantifiedExpression
class	TheorySideEffectExpression
class	TheoryTempVariableReference
class	TheoryUnaryExpression
class	TheoryVariableReference
class	TheoryVariantExpression

Fields in org.jmlspecs.jml4.fspv.theory declared as TheoryExpression

TheoryExpression	TheoryQuantifiedExpression.body
TheoryExpression	TheoryWhileStatement.condition
TheoryExpression	TheoryConditionalStatement.condition
static TheoryExpression[]	TheoryExpression.EMPTY
TheoryExpression	TheoryOldExpression.expression
TheoryExpression[]	TheoryBlockExpression.expressions
TheoryExpression	TheoryVariable.initialization
TheoryExpression	TheoryBinaryExpression.lhs
TheoryExpression	TheoryAssignmentStatement.lhs
TheoryExpression	TheoryLemma.post
TheoryExpression	TheoryLemma.pre
TheoryExpression	TheoryQuantifiedExpression.range
TheoryExpression	TheoryBinaryExpression.rhs
TheoryExpression	TheoryAssignmentStatement.rhs

Methods in org.jmlspecs.jml4.fspv.theory that return TheoryExpression

TheoryExpression	TheoryBlockExpression.expressionAt(int i)
TheoryExpression	TheoryLoopAnnotationsExpression.invariantAt(int i)
TheoryExpression	TheoryHelper.popExpression()
TheoryExpression	TheoryLoopAnnotationsExpression.variantAt(int i)
static TheoryExpression	TheoryLiteral.Zero(TheoryType type)

Methods in org.jmlspecs.jml4.fspv.theory with parameters of type TheoryExpression

java.lang.Object	TheoryVisitor.accept(TheoryExpression theoryExpression)
static TheoryVariable	TheoryVariable.Bound(java.lang.String name, TheoryType type, TheoryExpression initialization, int declSourceStart)
static TheoryVariable	TheoryVariable.Local(java.lang.String name, TheoryType type, TheoryExpression initialization, int declSourceStart)
void	TheoryHelper.push(TheoryExpression e)

Constructors in org.jmlspecs.jml4.fspv.theory with parameters of type TheoryExpression

TheoryAssignmentStatement(TheoryExpression l, TheoryExpression r)

TheoryBinaryExpression(TheoryExpression l, TheoryOperator op, TheoryExpression r)

TheoryBlockExpression(TheoryExpression[] expressions, TheoryType type)

TheoryConditionalStatement(TheoryExpression condition, TheoryBlockStatement thenBlock, TheoryBlockStatement elseBlock)

TheoryInvariantExpression(TheoryExpression[] expressions)

TheoryLemma(TheoryVariable[] variables, java.lang.String name, TheoryExpression pre, TheoryBlockStatement block, TheoryExpression post)

TheoryOldExpression(TheoryExpression e)

TheoryQuantifiedExpression(TheoryQuantifier quantifier, TheoryVariable variable, TheoryExpression range, TheoryExpression body)

TheoryVariable(java.lang.String name, TheoryType type2, TheoryExpression initialization, int kind, int declSourceStart)

TheoryVariantExpression(TheoryExpression[] expressions)

TheoryWhileStatement(TheoryExpression condition, TheoryLoopAnnotationsExpression loopAnnotations, TheoryBlockStatement block)