Uses of Class
fmrisc.ProgramExplorer.Syntax.Name

Packages that use Name

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

Uses of Name in fmrisc.ProgramExplorer.InOut

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

Modifier and Type	Method and Description
void	PrettyMathML.appendName(org.w3c.dom.Node parent, Name name) Convert nameto DOM representation of HTML/MathML markup.
void	Breaks.visit(Name exp)
void	PrettyPrinter.visit(Name exp)
void	PrettyMathML.visit(Name exp)

Uses of Name in fmrisc.ProgramExplorer.Judgements

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

Modifier and Type	Method and Description
static VariableSymbol	Normalization.modifiableVariable(Name name0) Derive the modifiable variable from a name.
static java.util.Set<VariableSymbol>	Normalization.modifiableVariables(Name[] names) Derive the modifiable variables of a method.
static void	Normalization.modifiableVariables(Name[] names, java.util.Set<VariableSymbol> vars) Derive the modifiable variables of a method.
static PostVariable	Satisfies.postVariable(Name name) Construct a post-variable.
static PreVariable	Satisfies.preVariable(Name name) Construct a pre-variable.

Uses of Name in fmrisc.ProgramExplorer.Parser

Methods in fmrisc.ProgramExplorer.Parser that return Name

Modifier and Type	Method and Description
Name	MiniJavaParser.name()
Name	SpecLangParser.name()

Methods in fmrisc.ProgramExplorer.Parser that return types with arguments of type Name

Modifier and Type	Method and Description
java.util.Vector<Name>	SpecLangParser.names()

Uses of Name in fmrisc.ProgramExplorer.Semantics

Methods in fmrisc.ProgramExplorer.Semantics that return Name

Modifier and Type	Method and Description
Name	GlobalSymbolBase.getLongName() Get the unique long name by which the symbol can be referenced.
Name	GlobalSymbol.getLongName() Get the unique long name by which the symbol can be referenced.
Name	GlobalVariableSymbolBase.getLongName() Get the unique long name by which the symbol can be referenced.

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

Modifier and Type	Method and Description
ClassSymbol	Environment.getClass(Name name) Return symbol for class denoted by name in current environment.
PackageSymbol	PackageSymbol.getPackage(Name name) Return symbol for package denoted by name in current package; an error message is printed if the lookup fails.
PackageSymbol	PackageSymbol.getPackage(Name name, boolean verbose) Return symbol for package denoted by name in current package.
VariableSymbol	Environment.getVariable(Name name) Return symbol for variable denoted by name in current environment.
VariableSymbol	Environment.getVariable(Name name, boolean verbose) Return symbol for variable denoted by name in current environment.
void	TCCGenerator.prove(java.lang.String name, SourcePosition position, Formula formula, StateType resultType, Name[] stateVars, Name[] stateExcs) Create a new task to prove the given formula.
void	TCCGenerator.prove(java.lang.String name, SourcePosition position, Formula formula, StateType resultType, Name[] stateVars, Name[] stateExcs) Create a new task to prove the given formula.
void	LogicChecking.setStateContext(Formula pre, StateType type, Name[] vars, Name[] excs, TaskFolder folder) Set the current program state context.
void	LogicChecking.setStateContext(Formula pre, StateType type, Name[] vars, Name[] excs, TaskFolder folder) Set the current program state context.
void	LogicTypeTable.setStateContext(StateType stateType, Name[] stateVars, Name[] stateExcs) Set the current state context.
void	LogicTypeTable.setStateContext(StateType stateType, Name[] stateVars, Name[] stateExcs) Set the current state context.
java.util.Vector<TheorySymbol>	LogicEnvironment.setTheories(PackageSymbol psymbol, TheorySymbol baseTheory, TheorySymbol classTheory, Import[] imports, Name[] tnames) Set in this environment the theories that may be referenced (ensuring that they are indeed read from file).

Constructors in fmrisc.ProgramExplorer.Semantics with parameters of type Name

Constructor and Description
GlobalSymbolBase(Identifier name, Name lname) Construct a symbol that can be externally referenced.

Uses of Name in fmrisc.ProgramExplorer.Syntax

Methods in fmrisc.ProgramExplorer.Syntax that return Name

Modifier and Type	Method and Description
static Name	Name.construct(Identifier ident) Construct name.
static Name	Name.construct(Identifier[] idents) Construct name.
static Name	Name.construct(Name prefix, Identifier ident) Construct name.
static Name	Name.construct(java.util.Vector<Identifier> idents) Construct name.
Name	Name.getPostfix() Get the postfix of the name.
Name	Name.getPrefix() Get the prefix of the name.
Name	Name.getPrefix(int n) Get prefix of first n identifiers of name.
static Name	NameUtils.getVariable(Name name) Determine variable prefix of name.
static Name	NameUtils.uniqueName(Name name) Get unique name by adding optional prefix.
static Name	NameUtils.uniqueName(VariableSymbol symbol) Get unique reference to program variable.

Methods in fmrisc.ProgramExplorer.Syntax that return types with arguments of type Name

Modifier and Type	Method and Description
static java.util.Set<Name>	NameUtils.getNames(java.util.Collection<TheorySymbol> symbols) Get names of symbols.

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

Modifier and Type	Method and Description
static Name	Name.construct(Name prefix, Identifier ident) Construct name.
boolean	Name.equals(Name name) Compare names for equality.
static java.util.Set<ClassSymbol>	NameUtils.getClassSymbols(Name[] names) Get set of class symbols denoted by names.
static java.util.Vector<TheorySymbol>	NameUtils.getTheorySymbols(Name[] names) Get vector of theory symbols denoted by names.
static Name	NameUtils.getVariable(Name name) Determine variable prefix of name.
static int	NameUtils.getVariablePosition(Name name) Determine variable prefix of name.
static VariableSymbol	NameUtils.getVariablePrefixSymbol(Name name) Determine variable prefix symbol of name.
static java.util.Set<VariableSymbol>	NameUtils.getVariablePrefixSymbols(Name[] names) Get set of variable symbols denoted by name.
static Name	NameUtils.uniqueName(Name name) Get unique name by adding optional prefix.
void	ASTVisitor.visit(Name tree)
void	ASTPrinter.visit(Name name) Print name (but do not print first identifier in name, if it is empty)
void	ASTCloner.visit(Name tree)
void	ASTVisitorBase.visit(Name tree)

Uses of Name in fmrisc.ProgramExplorer.Syntax.Logic

Methods in fmrisc.ProgramExplorer.Syntax.Logic that return Name

Modifier and Type	Method and Description
Name	StateThrowsException.getException() Get the name of the exception.
Name	ProgramVariable.getName() Get name of variable.
Name	Reference.getName() Get name of the variable.
Name	ProgramVariableBase.getName() Get name of variable.
Name[]	WritesOnlyFormula.getVariables() Get names of variables that are allowed to change.

Methods in fmrisc.ProgramExplorer.Syntax.Logic with parameters of type Name

Modifier and Type	Method and Description
static PreVariable	PreVariable.construct(Name name) Construct a reference to a program variable in the pre-state.
static PostVariable	PostVariable.construct(Name name) Construct a reference to a program variable in the post-state.
static Reference	Reference.construct(Name name) Construct a reference to a logical variable (or constant).
static WritesOnlyFormula	WritesOnlyFormula.construct(Name[] variables) Construct "writesonly" formula.
static StateThrowsException	StateThrowsException.construct(Term arg, Name exception) Construct the statement that a state throws a particular exception

Uses of Name in fmrisc.ProgramExplorer.Syntax.Program

Fields in fmrisc.ProgramExplorer.Syntax.Program declared as Name

Modifier and Type	Field and Description
Name	CallStatement.method
Name	NamedType.name
Name	CompilationUnitBase.pname

Methods in fmrisc.ProgramExplorer.Syntax.Program that return Name

Modifier and Type	Method and Description
Name	ImportBase.getName() Get the name denoted by the import statement.
Name	Import.getName() Get the name denoted by the import statement.
Name	CompilationUnit.getPackage() Get package name of unit
Name	CompilationUnitBase.getPackage() Get package name of unit

Methods in fmrisc.ProgramExplorer.Syntax.Program with parameters of type Name

Modifier and Type	Method and Description
static AssignCallStatement	AssignCallStatement.construct(LeftValue lval, Name method, ValueExpression[] args) Construct a call statement with a result value assigned to a variable.
static AssignNewStatement	AssignNewStatement.construct(LeftValue lval, Name type, ValueExpression[] args) Construct a call statement with a result value assigned to a variable.
static AssignCallStatement	AssignCallStatement.construct(LeftValue lval, Name method, java.util.Vector<ValueExpression> args) Construct a call statement with a result value assigned to a variable.
static AssignNewStatement	AssignNewStatement.construct(LeftValue lval, Name type, java.util.Vector<ValueExpression> args) Construct a call statement with a result value assigned to a variable.
static PackageImport	PackageImport.construct(Name name) Construct import with denoted name.
static NamedType	NamedType.construct(Name name) Construct a named type.
static ClassImport	ClassImport.construct(Name name) Construct import with denoted name.
static ClassDeclaration	ClassDeclaration.construct(Name pname, Import[] imports, Identifier name, TopDeclaration[] decls) Construct a class declaration
static ThrowStatement	ThrowStatement.construct(Name name, ValueExpression value) Construct a throw (exception) statement.
static VoidCallStatement	VoidCallStatement.construct(Name method, ValueExpression[] args) Construct a call statement without a result value.
static ClassDeclaration	ClassDeclaration.construct(Name pname, java.util.Vector<Import> imports, Identifier name, java.util.Vector<TopDeclaration> decls) Construct a class declaration
static VoidCallStatement	VoidCallStatement.construct(Name method, java.util.Vector<ValueExpression> args) Construct a call statement without a result value.
static DeclNewStatement	DeclNewStatement.construct(TypeExpression type, Identifier var, Name method, ValueExpression[] args) Construct a call statement with a result value assigned to a variable.
static DeclCallStatement	DeclCallStatement.construct(TypeExpression type, Identifier var, Name method, ValueExpression[] args) Construct a call statement with a result value assigned to a variable.
static DeclNewStatement	DeclNewStatement.construct(TypeExpression type, Identifier var, Name method, java.util.Vector<ValueExpression> args) Construct a call statement with a result value assigned to a variable.
static DeclCallStatement	DeclCallStatement.construct(TypeExpression type, Identifier var, Name method, java.util.Vector<ValueExpression> args) Construct a call statement with a result value assigned to a variable.

Uses of Name in fmrisc.ProgramExplorer.Syntax.Spec

Methods in fmrisc.ProgramExplorer.Syntax.Spec that return Name

Modifier and Type	Method and Description
Name[]	MethodSpec.getExceptions() Get list of exceptions that may be thrown by method.
Name[]	UnitSpec.getTheories() Get theories referenced by unit.
Name[]	TheoryDeclaration.getTheories() Get theories on which unit depends.
Name[]	MethodSpec.getVariables() Get method frame i.e.

Methods in fmrisc.ProgramExplorer.Syntax.Spec with parameters of type Name

Modifier and Type	Method and Description
static TheoryDeclaration	TheoryDeclaration.construct(Name pname, Import[] imports, Identifier name, Name[] theories, Declaration[] decls) Construct a theory declaration
static TheoryDeclaration	TheoryDeclaration.construct(Name pname, Import[] imports, Identifier name, Name[] theories, Declaration[] decls) Construct a theory declaration
static TheoryDeclaration	TheoryDeclaration.construct(Name pname, java.util.Vector<Import> imports, Identifier name, java.util.Vector<Name> theories, java.util.Vector<Declaration> decls) Construct a theory.

Method parameters in fmrisc.ProgramExplorer.Syntax.Spec with type arguments of type Name

Modifier and Type	Method and Description
static TheoryDeclaration	TheoryDeclaration.construct(Name pname, java.util.Vector<Import> imports, Identifier name, java.util.Vector<Name> theories, java.util.Vector<Declaration> decls) Construct a theory.
void	MethodSpec.setExceptions(java.util.Vector<Name> es) Set exceptions
void	UnitSpec.setTheories(java.util.Vector<Name> ts) Set theories referenced by unit.
void	MethodSpec.setVariables(java.util.Vector<Name> vs) Set specification variables.

Uses of Name in fmrisc.ProgramExplorer.Tasks

Methods in fmrisc.ProgramExplorer.Tasks with parameters of type Name

Modifier and Type	Method and Description
static void	PreconditionTasks.generate(ParamSymbol method, java.util.Map<Statement,Formula> preMap, StateType stateType, Name[] stateVars, Name[] stateExcs, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, ErrorStream out) Construct the precondition tasks for a given method.
static void	PreconditionTasks.generate(ParamSymbol method, java.util.Map<Statement,Formula> preMap, StateType stateType, Name[] stateVars, Name[] stateExcs, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, ErrorStream out) Construct the precondition tasks for a given method.
static void	TerminationTasks.register(ParamSymbol method, StateType stateType, Name[] stateVars, Name[] stateExcs, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, ErrorStream out) Register the construction of termination tasks for a given method.
static void	TerminationTasks.register(ParamSymbol method, StateType stateType, Name[] stateVars, Name[] stateExcs, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, ErrorStream out) Register the construction of termination tasks for a given method.
static void	MethodTasks.register(ParamSymbol method, StateType stateType, Name[] stateVars, Name[] stateExcs, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, ErrorStream out) Register the construction of tasks for a given method.
static void	MethodTasks.register(ParamSymbol method, StateType stateType, Name[] stateVars, Name[] stateExcs, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, ErrorStream out) Register the construction of tasks for a given method.

Constructors in fmrisc.ProgramExplorer.Tasks with parameters of type Name

Constructor and Description
CorrectnessTask(ParamSymbol method, java.io.File parent, StateType stateType, Name[] stateVars, Name[] stateExcs, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, ErrorStream out) Construct a partial correctness task for a given method.
CorrectnessTask(ParamSymbol method, java.io.File parent, StateType stateType, Name[] stateVars, Name[] stateExcs, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, ErrorStream out) Construct a partial correctness task for a given method.
TypeCheckingTask(TheorySymbol tsymbol, java.lang.String name, SourcePosition position, java.io.File dir, StateType resultType, Name[] stateVars, Name[] stateExcs, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, Formula goal, ErrorStream out) Create task of proving a type-checking condition.
TypeCheckingTask(TheorySymbol tsymbol, java.lang.String name, SourcePosition position, java.io.File dir, StateType resultType, Name[] stateVars, Name[] stateExcs, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, Formula goal, ErrorStream out) Create task of proving a type-checking condition.