Uses of Interface
fmrisc.ProgramExplorer.Semantics.VariableSymbol

Packages that use VariableSymbol

Package	Description
fmrisc.ProgramExplorer.Judgements
fmrisc.ProgramExplorer.Proving
fmrisc.ProgramExplorer.Semantics
fmrisc.ProgramExplorer.Syntax
fmrisc.ProgramExplorer.Tasks

Uses of VariableSymbol in fmrisc.ProgramExplorer.Judgements

Fields in fmrisc.ProgramExplorer.Judgements with type parameters of type VariableSymbol

Modifier and Type	Field and Description
java.util.Set<VariableSymbol>	StatJudgement.variables

Methods in fmrisc.ProgramExplorer.Judgements that return VariableSymbol

Modifier and Type	Method and Description
static VariableSymbol	Normalization.modifiableVariable(Name name0) Derive the modifiable variable from a name.

Methods in fmrisc.ProgramExplorer.Judgements that return types with arguments of type VariableSymbol

Modifier and Type	Method and Description
static java.util.Set<VariableSymbol>	Normalization.modifiableVariables(Name[] names) Derive the modifiable variables of a method.

Method parameters in fmrisc.ProgramExplorer.Judgements with type arguments of type VariableSymbol

Modifier and Type	Method and Description
StatJudgement	Satisfies.extendFrame(StatJudgement S, java.util.Set<VariableSymbol> vars) Extend judgement to the denoted set of modifiable variables.
static void	Normalization.modifiableVariables(Name[] names, java.util.Set<VariableSymbol> vars) Derive the modifiable variables of a method.
static Expression	Substitution.perform(Expression exp, Term oldStateTerm, Term newStateTerm, java.util.Map<VariableSymbol,Substitution.Value> vars) Create a copy of expression with the denoted substitutions performed.
static Formula	Normalization.perform(Formula formula, java.util.Collection<VariableSymbol> variables) Replace copy of formula with all poststate variables that do not appear in the set of modifiable variables replaced by prestate variables.

Constructor parameters in fmrisc.ProgramExplorer.Judgements with type arguments of type VariableSymbol

Constructor and Description
StatJudgement(Formula precondition, Formula formula, boolean executes, boolean continues, boolean breaks, boolean returns, java.util.Set<ClassSymbol> exceptions, java.util.Set<VariableSymbol> variables) Construct a command specification.

Uses of VariableSymbol in fmrisc.ProgramExplorer.Proving

Constructor parameters in fmrisc.ProgramExplorer.Proving with type arguments of type VariableSymbol

Constructor and Description
StateProblem(Declaration[] decls, Formula goal, java.util.Map<Symbol,Symbol> map, StateType stateType, Type stringType, java.util.Collection<VariableSymbol> variables, java.util.Collection<ClassSymbol> exceptions, ErrorStream out) Construct a proving problem.

Uses of VariableSymbol in fmrisc.ProgramExplorer.Semantics

Classes in fmrisc.ProgramExplorer.Semantics that implement VariableSymbol

Modifier and Type	Class and Description
class	BodySymbol The symbol for a variable introduced in a method/constructor body.
class	ClassVariableSymbol A class value.
class	GlobalVariableSymbolBase The base class of a variable symbol that can be externally referenced.
class	LocalVariableSymbolBase The base class for a variable symbol that can be only locally referenced.
class	ObjectVariableSymbol An object value.
class	ParameterSymbol The symbol for a method/constructor parameter.
class	ThisSymbol The symbol for "this" object in a non-static context.
class	VariableSymbolBase A symbol denoting a variable.

Methods in fmrisc.ProgramExplorer.Semantics that return VariableSymbol

Modifier and Type	Method and Description
VariableSymbol	Environment.getVariable(Identifier ident) Return symbol for variable denoted by identifier in current environment.
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.

Methods in fmrisc.ProgramExplorer.Semantics that return types with arguments of type VariableSymbol

Modifier and Type	Method and Description
static java.util.Set<VariableSymbol>	VariableSymbolBase.apply(java.util.Map<Symbol,Symbol> map, java.util.Set<VariableSymbol> symbols) Apply map to set of variable symbols.
static java.util.Collection<VariableSymbol>	ReferencedVars.compute(AST tree) Compute referenced variables
java.util.Collection<VariableSymbol>	ReferencedVars.getResult() Get the result of the computation.

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

Modifier and Type	Method and Description
static java.lang.String[]	NewVariables.newVariables(VariableSymbol[] vars, java.lang.String suffix, java.util.Collection<java.lang.String> used) Compute unique and unused variable names.

Method parameters in fmrisc.ProgramExplorer.Semantics with type arguments of type VariableSymbol

Modifier and Type	Method and Description
static java.util.Set<VariableSymbol>	VariableSymbolBase.apply(java.util.Map<Symbol,Symbol> map, java.util.Set<VariableSymbol> symbols) Apply map to set of variable symbols.

Uses of VariableSymbol in fmrisc.ProgramExplorer.Syntax

Methods in fmrisc.ProgramExplorer.Syntax that return VariableSymbol

Modifier and Type	Method and Description
static VariableSymbol	NameUtils.getVariablePrefixSymbol(Name name) Determine variable prefix symbol of name.

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

Modifier and Type	Method and Description
static java.util.Set<VariableSymbol>	NameUtils.getVariablePrefixSymbols(Name[] names) Get set of variable symbols denoted by name.

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

Modifier and Type	Method and Description
static Name	NameUtils.uniqueName(VariableSymbol symbol) Get unique reference to program variable.

Uses of VariableSymbol in fmrisc.ProgramExplorer.Tasks

Constructor parameters in fmrisc.ProgramExplorer.Tasks with type arguments of type VariableSymbol

Constructor and Description
InvariantTask(ParamSymbol method, Statement stat, Formula goal, Formula invariant, SourcePosition pos, Formula cond, Formula body, java.io.File parent, StateType stateType, java.util.Set<VariableSymbol> variables, java.util.Set<ClassSymbol> exceptions, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, ErrorStream out) Construct an invariant verification task.
TerminationTask(java.lang.String kind, ParamSymbol method, Formula goal, Statement stat, java.lang.String tag, java.io.File parent, StateType stateType, java.util.Set<VariableSymbol> variables, java.util.Set<ClassSymbol> exceptions, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, ErrorStream out) Construct a termination verification task.