Package  Description 

fmrisc.ProgramExplorer.Syntax  
fmrisc.ProgramExplorer.Syntax.Logic 
Modifier and Type  Method and Description 

void 
ASTVisitor.visit(ExpressionBase tree) 
void 
ASTVisitorBase.visit(ExpressionBase tree) 
Modifier and Type  Class and Description 

class 
AndFormula
A logical conjunction.

class 
ApplicationExpression
An application of one expression to some other expression(s).

class 
ArrayTerm
An array term.

class 
ArrayType
An array type.

class 
AtomicFormula
An atomic formula.

class 
AtomicType
An atomic type.

class 
BinaryAtomicFormula
Base class of atomic formulas with binary operators.

class 
BinaryExpression
Base class of binary expressions.

class 
BinaryFormula
Base class of binary formulas.

class 
BinaryTerm
Base class of binary terms.

class 
BitAndTerm
A bit conjunction term.

class 
BitFalse
A literal denoting the bit value "0".

class 
BitLiteral
A bit (i.e., 0,1) value.

class 
BitNegationTerm
A bit negation term.

class 
BitOrTerm
A bit disjunction term.

class 
BitTrue
A literal denoting the bit value "1".

class 
BitType
The type of bit values.

class 
BooleanLiteral
A logical (i.e.

class 
BooleanType
The type of truth values.

class 
Constant
A constant.

class 
DividesTerm
A quotient term.

class 
EqualsFormula
An equality.

class 
EquivalentFormula
A logical equivalence.

class 
ExistsFormula
An existentially quantified formula.

class 
False
A literal denoting the boolean value "false".

class 
ForallFormula
A universally quantified formula.

class 
FormulaBase
Base class of a logical formula.

class 
FunctionApplication
A function application.

class 
FunctionType
A function type.

class 
GreaterEqualFormula
An isgreaterthanorequal formula.

class 
GreaterFormula
An isgreaterthan formula.

class 
IfThenElseExpression
Base class of a conditional expression.

class 
IfThenElseFormula
Base class of a conditional formula.

class 
IfThenElseTerm
Base class of a conditional term.

class 
ImpliesFormula
A logical implication.

class 
IntLiteral
A natural number.

class 
IntType
The type of integers.

class 
LambdaFormula
A function expression with a formula body.

class 
LambdaTerm
A function expression.

class 
LessEqualFormula
An islessthanorequal formula.

class 
LessFormula
An islessthan formula.

class 
LetExpression
Base class of an expression with local definitions.

class 
LetFormula
A formula with local value definitions.

class 
LetTerm
A term with local value definitions.

class 
MinusTerm
A difference term.

class 
NatType
The type of natural numbers.

class 
NegationTerm
An arithmetic negation term.

class 
NewState
A state literal referring to the new (successor) state.

class 
NotEqualsFormula
An equality.

class 
NotEquivalentFormula
An exclusive disjunction.

class 
NotFormula
A logical negation.

class 
OldState
A state literal referring to the old (predecessor) state.

class 
OrFormula
A logical disjunction.

class 
PlusTerm
A sum term.

class 
PostfixApplication
A postfix application of one expression to some other expression.

class 
PostfixFormula
A postfix application of a predicate.

class 
PostfixTerm
A postfix application of a function

class 
PostVariable
A reference to a program variable in the poststate.

class 
PowerTerm
An exponent term.

class 
PreVariable
A reference to a program variable in the prestate.

class 
ProgramVariableBase
Base class of a reference to a program variable.

class 
QuantifiedExpression
Base class of quantified expressions.

class 
QuantifiedFormula
Base class of quantified formulas.

class 
QuantifiedTerm
Base class of quantified terms.

class 
ReadsOnlyFormula
A formula that states that no program variable may change.

class 
Real0Type
The type of reals including the results of divisions by zero (intenally used).

class 
RealType
The type of reals.

class 
RecordTerm
A record of named values.

class 
RecordType
A record type.

class 
Reference
A reference to a logical variable (or constant).

class 
SelectionTerm
A term from which a component is selected.

class 
SimilarFormula
A state similarity (equality up to result value).

class 
StateBreaks
The statement that a state is "breaking".

class 
StateContinues
The statement that a state is "continuing".

class 
StateExecutes
The statement that a state is "executing".

class 
StateLiteral
A literal referring to a state.

class 
StateMessage
The exception message captured by a state.

class 
StateReturns
The statement that a state is "returning".

class 
StateThrows
The statement that a state is "throwing".

class 
StateThrowsException
The statement that a state throws a particular exception.

class 
StateType
The type of state values.

class 
StateValue
A reference to the return value captured by the current state.

class 
StringLiteral
A natural number.

class 
StringType
The type of character strings.

class 
SubrangeType
An subrange type.

class 
SubType
An subtype.

class 
TermApplication
An application of one term to some other term(s).

class 
TermBase
Base class of a value term.

class 
TimesTerm
A product term.

class 
True
A literal denoting the boolean value "true".

class 
TupleTerm
A tuple of values.

class 
TupleType
A tuple type.

class 
TypeBase
Base class of a type (term).

class 
UnaryExpression
Base class of unary expressions.

class 
UnaryFormula
Base class of unary formulas.

class 
UnaryTerm
Base class of unary terms.

class 
UpdateTerm
A term from which a component is updated.

class 
WritesOnlyFormula
A formula that states that only certain program variables may change.
