Uses of Interface
fmrisc.ProgramExplorer.Syntax.AST

Packages that use AST

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

Uses of AST in fmrisc.ProgramExplorer.InOut

Fields in fmrisc.ProgramExplorer.InOut declared as AST

Modifier and Type	Field and Description
AST	Breaks.Info.tree

Methods in fmrisc.ProgramExplorer.InOut with parameters of type AST

Modifier and Type	Method and Description
void	ASTPrinterHTML.append(AST tree) Append tree to output.

Constructors in fmrisc.ProgramExplorer.InOut with parameters of type AST

Constructor and Description
Info(AST tree) Create info for the denoted tree.

Uses of AST in fmrisc.ProgramExplorer.Judgements

Classes in fmrisc.ProgramExplorer.Judgements that implement AST

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

Methods in fmrisc.ProgramExplorer.Judgements that return AST

Modifier and Type	Method and Description
static AST	RefSubstitution.perform(java.util.Map<java.lang.String,Term> map, AST exp) Perform substitution of identifiers by terms.

Methods in fmrisc.ProgramExplorer.Judgements with parameters of type AST

Modifier and Type	Method and Description
static AST	RefSubstitution.perform(java.util.Map<java.lang.String,Term> map, AST exp) Perform substitution of identifiers by terms.

Uses of AST in fmrisc.ProgramExplorer.Semantics

Methods in fmrisc.ProgramExplorer.Semantics that return AST

Modifier and Type	Method and Description
static AST	PreStateCloner.clone(AST tree) Create a clone (deep copy) of a tree denoting a logic entity replacing all post-state references by prestate references.
static AST	PostStateCloner.clone(AST tree) Create a clone (deep copy) of a tree denoting a logic entity replacing all pre-state references by post-state references.
static AST	TypeCloner.clone(AST tree, java.util.Map<Symbol,Symbol> map) Create a clone (deep copy) of a tree replacing references to certain symbols.
static AST	ReferenceCloner.clone(AST tree, java.util.Map<Symbol,Symbol> map) Create a clone (deep copy) of a tree replacing references to certain symbols.

Methods in fmrisc.ProgramExplorer.Semantics with parameters of type AST

Modifier and Type	Method and Description
void	ReferencedVars.add(AST tree) Add references from the denoted tree.
void	ReferencedExcs.add(AST tree) Add references from the denoted tree.
static AST	PreStateCloner.clone(AST tree) Create a clone (deep copy) of a tree denoting a logic entity replacing all post-state references by prestate references.
static AST	PostStateCloner.clone(AST tree) Create a clone (deep copy) of a tree denoting a logic entity replacing all pre-state references by post-state references.
static AST	TypeCloner.clone(AST tree, java.util.Map<Symbol,Symbol> map) Create a clone (deep copy) of a tree replacing references to certain symbols.
static AST	ReferenceCloner.clone(AST tree, java.util.Map<Symbol,Symbol> map) Create a clone (deep copy) of a tree replacing references to certain symbols.
static java.util.Collection<VariableSymbol>	ReferencedVars.compute(AST tree) Compute referenced variables
static java.util.Collection<Symbol>	ReferencedUnits.compute(AST tree) Compute referenced units.
static java.util.Collection<ClassSymbol>	ReferencedExcs.compute(AST tree) Compute referenced exceptions.
static void	VariableTypes.process(AST tree, TypeTranslator trans) Set the logical types of all variable symbols.

Uses of AST in fmrisc.ProgramExplorer.Syntax

Subinterfaces of AST in fmrisc.ProgramExplorer.Syntax

Modifier and Type	Interface and Description
interface	ASTSource Interface to abstract syntax trees that are linked to the source code.
interface	Declaration The interface to declarations.

Classes in fmrisc.ProgramExplorer.Syntax that implement AST

Modifier and Type	Class and Description
class	ASTBase Base class for abstract syntax trees.
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.

Methods in fmrisc.ProgramExplorer.Syntax that return AST

Modifier and Type	Method and Description
static AST	ASTCloner.clone(AST tree) Create a clone (deep copy) of a tree denoting a logic entity.

Methods in fmrisc.ProgramExplorer.Syntax with parameters of type AST

Modifier and Type	Method and Description
static void	ASTBase.accept(AST[] trees, ASTVisitor visitor) Visit a sequence of abstract syntax trees.
static void	ASTBase.accept(AST[] trees, ASTVisitorOld visitor) Visit a sequence of abstract syntax trees.
static AST	ASTCloner.clone(AST tree) Create a clone (deep copy) of a tree denoting a logic entity.
static void	ASTPrinter.print(AST tree, java.io.PrintWriter out, ASTPrinter.PrintStatementSpec printStatSpec, boolean printAnnotation) Print tree on writer including specification commands.
boolean	ASTVisitorBaseOld.visit(AST tree) Visit an abstract syntax tree.
boolean	ASTVisitorOld.visit(AST tree) Visit an abstract syntax tree.
void	ASTVisitor.visit(AST tree) Visit an abstract syntax tree.
void	ASTVisitorBase.visit(AST tree) Visit an abstract syntax tree.

Uses of AST in fmrisc.ProgramExplorer.Syntax.Logic

Subinterfaces of AST in fmrisc.ProgramExplorer.Syntax.Logic

Modifier and Type	Interface and Description
interface	ASTLogic Interface to any kind of logical syntax.
interface	Definition Interface to any kind of logical definition.
interface	Expression Interface to any kind of logical expression.
interface	Formula Interface to a logical formula.
interface	ProgramVariable Interface to any expression denoting a storage location.
interface	Selector Interface to a component selector.
interface	Term Interface to a value term.
interface	Type Interface to a type term.
interface	ValueDeclaration Interface to a value declaration.
interface	ValueDefinition Interface to a value definition.

Classes in fmrisc.ProgramExplorer.Syntax.Logic that implement AST

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 AST in fmrisc.ProgramExplorer.Syntax.Program

Subinterfaces of AST in fmrisc.ProgramExplorer.Syntax.Program

Modifier and Type	Interface and Description
interface	ASTProgram Interface to abstract syntax trees of programs.
interface	ASTProgramAnnotated Interface to abstract syntax trees that may have an annotation.
interface	CompilationUnit Interface to a compilation unit.
interface	Import Interface to an import statement.
interface	LoopStatement The interface for loop statements
interface	ParamDeclaration The interface to declarations with parameters
interface	ProgramAnnotation Interface to a program annotation
interface	ProgramDeclaration Interface to a program declaration.
interface	Statement An interface to program statements
interface	TopDeclaration The interface to declarations.
interface	TypeExpression An interface to expressions denoting types.
interface	ValueExpression An interface to expressions denoting values.
interface	VariableDeclaration The interface to declarations introducing variables with types

Classes in fmrisc.ProgramExplorer.Syntax.Program that implement AST

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 AST in fmrisc.ProgramExplorer.Syntax.Spec

Subinterfaces of AST in fmrisc.ProgramExplorer.Syntax.Spec

Modifier and Type	Interface and Description
interface	Specification The interface to specifications.

Classes in fmrisc.ProgramExplorer.Syntax.Spec that implement AST

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.