Uses of Class
fmrisc.ProgramExplorer.Syntax.ASTBase

Packages that use ASTBase

Package	Description
fmrisc.ProgramExplorer.Judgements
fmrisc.ProgramExplorer.Syntax
fmrisc.ProgramExplorer.Syntax.Logic
fmrisc.ProgramExplorer.Syntax.Program
fmrisc.ProgramExplorer.Syntax.Spec

Uses of ASTBase in fmrisc.ProgramExplorer.Judgements

Subclasses of ASTBase in fmrisc.ProgramExplorer.Judgements

Modifier and Type	Class and Description
class	StatJudgement A statement judgement.

Uses of ASTBase in fmrisc.ProgramExplorer.Syntax

Subclasses of ASTBase in fmrisc.ProgramExplorer.Syntax

Modifier and Type	Class and Description
class	ASTSourceBase Base class of abstract syntax trees that are linked to the source code.
class	Identifier A simple (unstructured) identifier.
class	Name A name i.e.

Uses of ASTBase in fmrisc.ProgramExplorer.Syntax.Logic

Subclasses of ASTBase in fmrisc.ProgramExplorer.Syntax.Logic

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	ASTLogicBase Base class of any kind of logical syntax.
class	AtomicFormula An atomic formula.
class	AtomicType An atomic type.
class	AxiomDefinition The definition of an axiom
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	DeclarationBase The base class of declarations.
class	DefinitionBase The base class of definitions.
class	DividesTerm A quotient term.
class	EqualsFormula An equality.
class	EquivalentFormula A logical equivalence.
class	ExistsFormula An existentially quantified formula.
class	ExpressionBase Base class of any kind of logical expression.
class	False A literal denoting the boolean value "false".
class	ForallFormula A universally quantified formula.
class	FormulaBase Base class of a logical formula.
class	FormulaDefinition The definition of a formula
class	FunctionApplication A function application.
class	FunctionType A function type.
class	GreaterEqualFormula An is-greater-than-or-equal formula.
class	GreaterFormula An is-greater-than 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 is-less-than-or-equal formula.
class	LessFormula An is-less-than 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 post-state.
class	PowerTerm An exponent term.
class	PreVariable A reference to a program variable in the pre-state.
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	SelectorBase Base class of component selectors.
class	SelectorIdentifier Selection by identifier.
class	SelectorIndex Selection by index.
class	SelectorNumber Selection by number.
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	TypeDeclaration The declaration of a type.
class	TypeDefinition The definition of a type.
class	TypedIdentifier An identifier with a type.
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	ValueDeclarationClass The declaration of a value.
class	ValueDeclarationFormula The declaration of a value (predicate) initialized by a formula
class	ValueDeclarationInitialized The declaration of a value with initialization.
class	ValueDefinitionClass The definition of a value.
class	ValuedIdentifier An identifier with a value.
class	WritesOnlyFormula A formula that states that only certain program variables may change.

Uses of ASTBase in fmrisc.ProgramExplorer.Syntax.Program

Subclasses of ASTBase in fmrisc.ProgramExplorer.Syntax.Program

Modifier and Type	Class and Description
class	AndExpression A logical conjunction.
class	AssertionStatement An assertion statement.
class	AssignCallStatement A method call statement with a result value assigned to a variable.
class	AssignmentStatement An assignment statement.
class	AssignNewStatement A constructor call statement with the result value assigned to a variable.
class	ASTProgramAnnotatedBase Base class of abstract syntax trees that may have an annotation.
class	ASTProgramBase Base class of abstract syntax trees of programs.
class	BinaryValueExpression The base class of binary expressions denoting values.
class	BlockStatement A block statement i.e.
class	BreakStatement A break statement.
class	CallStatement An method call statement.
class	CharLiteral A character literal.
class	CharType The type of character values
class	ClassDeclaration A class declaration
class	ClassImport Import of a single class.
class	ClassMethodDeclaration A class method declaration.
class	ClassVariableDeclaration A class variable declaration.
class	CompilationUnitBase Base class of a compilation unit.
class	ConditionalStatement A conditional statement with one or two branches.
class	ConstructorDeclaration A constructor declaration.
class	ContinueStatement A continue statement.
class	DeclCallStatement A method call statement with a result value initializing a local variable.
class	DeclNewStatement A constructor call statement with a result value initializing a local variable.
class	DividesExpression A quotient expression.
class	EmptyStatement An empty statement (skip).
class	EqualsExpression An equality.
class	ExceptionType The (base) type of exceptions.
class	ForLoopStatement A for loop.
class	GlobalVariableDeclaration A global variable declaration.
class	GreaterEqualExpression An is-greater-than-or-equal formula.
class	GreaterExpression An is-greater-than formula.
class	Handler An exception handler.
class	IdentifierSelector Component selection by name.
class	ImportBase Base class of import statements.
class	IndexSelector Component selection by index.
class	LeftValue The left value of an assignment.
class	LessEqualExpression An is-less-than-or-equal formula.
class	LessExpression An is-less-than formula.
class	LoopStatementBase The base class for loop statements.
class	MessageSelector Selection of a message from an exception.
class	MethodDeclaration A method declaration.
class	MinusExpression A difference expression.
class	NamedType A named (user-defined) type
class	NegationExpression An arithmetic negation expression.
class	NewArrayExpression Allocation of a new array.
class	NewType The type of a new object.
class	NotEqualsExpression An inequality.
class	NotExpression A logical negation.
class	NullLiteral A null literal (for objects/arrays/strings)
class	NullType The type of the literal "null"
class	ObjectMethodDeclaration An object method declaration.
class	ObjectVariableDeclaration An object variable declaration.
class	OrExpression A logical disjunction.
class	PackageImport Import of all classes of a package.
class	ParamDeclarationBase The base class for a declaration with parameters.
class	Parameter A parameter i.e.
class	PercentExpression A remainder expression.
class	PlusExpression A sum expression.
class	PrimitiveType A primitive (built-in) type
class	ProgramAnnotationBase A program annotation.
class	ReturnStatement A return statement with an optional return value.
class	SelectorExpression Selection of an object component
class	StatementBase The base class for statements.
class	ThrowStatement A throw (exception statement)
class	TimesExpression A product expression.
class	TopDeclarationBase A top-level declaration inside a class.
class	TryCatchStatement A protected code block.
class	UnaryValueExpression The base class of unary expressions denoting values.
class	ValueExpressionBase The base class of expressions denoting values.
class	VariableDeclarationBase The base class of declarations introducing variables with types.
class	VariableStatement A local variable declaration
class	VariableValue A variable denoting a value.
class	VoidCallStatement A method call statement without a result value.
class	VoidType The type with no values
class	WhileLoopStatement A while loop.

Uses of ASTBase in fmrisc.ProgramExplorer.Syntax.Spec

Subclasses of ASTBase in fmrisc.ProgramExplorer.Syntax.Spec

Modifier and Type	Class and Description
class	ClassSpec A class specification.
class	LoopSpec A loop specification.
class	MethodSpec A method specification.
class	SpecificationBase The base class of specifications.
class	StatementSpec A statement specification.
class	TheoryDeclaration The declaration of a logical theory.
class	UnitSpec A unit specification.