Package | Description |
---|---|
fmrisc.ProgramExplorer | |
fmrisc.ProgramExplorer.Proving | |
fmrisc.ProgramExplorer.Semantics | |
fmrisc.ProgramExplorer.SWT | |
fmrisc.ProgramExplorer.Syntax | |
fmrisc.ProgramExplorer.Tasks |
Modifier and Type | Method and Description |
---|---|
static Symbol |
Main.getUnit(PackageSymbol top,
java.lang.String name,
boolean theory)
Get symbol of unit denoted by qualified name in top-level package.
|
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.
|
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.
|
Modifier and Type | Class and Description |
---|---|
class |
SymbolTable<S extends Symbol>
A symbol table.
|
Modifier and Type | Interface and Description |
---|---|
interface |
GlobalSymbol
The interface to a symbol that can be globally referenced.
|
interface |
VariableSymbol
The interface to a symbol denoting a variable.
|
Modifier and Type | Class and Description |
---|---|
class |
AxiomSymbol
A symbol denoting a logical axiom.
|
class |
BodySymbol
The symbol for a variable introduced in a method/constructor body.
|
class |
ClassMethodSymbol
A symbol denoting a class method.
|
class |
ClassSymbol
A symbol denoting a class.
|
class |
ClassVariableSymbol
A class value.
|
class |
ConstructorSymbol
A symbol denoting a class constructor.
|
class |
FormulaSymbol
A symbol denoting a logical formula.
|
class |
GlobalSymbolBase
The base class of a symbol that can be globally referenced.
|
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 |
MethodSymbol
A symbol denoting a method.
|
class |
ObjectMethodSymbol
A symbol denoting an object method.
|
class |
ObjectVariableSymbol
An object value.
|
class |
PackageSymbol
A symbol denoting a value.
|
class |
ParameterSymbol
The symbol for a method/constructor parameter.
|
class |
ParamSymbol
A symbol denoting a parameterized entity.
|
class |
SymbolBase
The base class of symbols.
|
class |
TheorySymbol
A symbol denoting a theory.
|
class |
ThisSymbol
The symbol for "this" object in a non-static context.
|
class |
TypeSymbol
A symbol denoting a logical type.
|
class |
ValueSymbol
A symbol denoting a logical value.
|
class |
VariableSymbolBase
A symbol denoting a variable.
|
Modifier and Type | Method and Description |
---|---|
static java.util.Collection<Symbol> |
ReferencedUnits.compute(AST tree)
Compute referenced units.
|
static java.util.Collection<Symbol> |
ReferencedUnits.filterDependencies(Symbol symbol,
java.util.Collection<Symbol> symbols)
Filter all those units that (directly or indirectly) depend on given unit.
|
java.util.Collection<Symbol> |
TheorySymbol.getReferencedUnits()
Get symbols of units referenced by this unit.
|
java.util.Collection<Symbol> |
ClassSymbol.getReferencedUnits()
Get symbols of units referenced by this unit.
|
Modifier and Type | Method and Description |
---|---|
static java.util.Collection<Symbol> |
ReferencedUnits.filterDependencies(Symbol symbol,
java.util.Collection<Symbol> symbols)
Filter all those units that (directly or indirectly) depend on given unit.
|
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.Set<VariableSymbol> |
VariableSymbolBase.apply(java.util.Map<Symbol,Symbol> map,
java.util.Set<VariableSymbol> symbols)
Apply map to set of variable symbols.
|
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 |
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 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 void |
ReferencedUnits.computeClosure(java.util.Collection<Symbol> in,
java.util.Vector<Symbol> out)
Compute closure of unit dependencies.
|
static void |
ReferencedUnits.computeClosure(java.util.Collection<Symbol> in,
java.util.Vector<Symbol> out)
Compute closure of unit dependencies.
|
static java.util.Collection<Symbol> |
ReferencedUnits.filterDependencies(Symbol symbol,
java.util.Collection<Symbol> symbols)
Filter all those units that (directly or indirectly) depend on given unit.
|
Modifier and Type | Method and Description |
---|---|
Symbol[] |
SymbolTree.getSelection()
Get symbols selected in tree.
|
Modifier and Type | Method and Description |
---|---|
java.util.Collection<Symbol> |
SymbolTree.getUnitSymbols()
Get all symbols in symbol tree denoting units (classes/theories).
|
Modifier and Type | Method and Description |
---|---|
void |
TaskTree.display(Symbol symbol)
Display task folder associated to symbol (if any).
|
void |
TopWindow.displayTasks(Symbol symbol)
Display the tasks associated to the symbol.
|
void |
TopWindow.print(Symbol symbol)
Print symbol on console.
|
void |
TopWindow.printDecl(Symbol symbol)
Print declaration/definition of symbol on console.
|
void |
SymbolTree.remove(Symbol symbol)
Remove subtree denoted by symbol.
|
void |
SymbolTree.show(Symbol symbol)
Show tree item denoted by symbol.
|
void |
SymbolTree.signalError(Symbol symbol)
Indicate that symbol has errors.
|
Modifier and Type | Method and Description |
---|---|
Symbol |
Name.getSymbol()
Get symbol identified by (last part of) name.
|
Symbol |
Identifier.getSymbol()
Get symbol denoted by identifier.
|
Modifier and Type | Method and Description |
---|---|
void |
Identifier.setSymbol(Symbol symbol)
Set symbol denoted by identifier (must not yet be set).
|
Modifier and Type | Field and Description |
---|---|
java.util.Map<Symbol,Symbol> |
FlattenDeclarations.Result.map |
java.util.Map<Symbol,Symbol> |
FlattenDeclarations.Result.map |
Modifier and Type | Method and Description |
---|---|
Symbol |
TaskFolder.getSymbol()
Get the symbol associated to the folder.
|
Constructor and Description |
---|
TaskFolder(Symbol symbol,
java.lang.String name,
java.io.File root)
Construct root folder.
|
TaskFolder(Symbol symbol,
java.lang.String name,
TaskFolder parent)
Construct sorted task folder with denoted name and parent
|
TaskFolder(Symbol symbol,
java.lang.String name,
TaskFolder parent,
boolean sorted)
Construct task folder with denoted name and parent
|
Constructor and Description |
---|
Result(Declaration[] decls,
Formula goal,
java.util.Map<Symbol,Symbol> map) |
Result(Declaration[] decls,
Formula goal,
java.util.Map<Symbol,Symbol> map) |