Uses of Class
fmrisc.ProgramExplorer.InOut.ErrorStream

Packages that use ErrorStream

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

Uses of ErrorStream in fmrisc.ProgramExplorer

Methods in fmrisc.ProgramExplorer that return ErrorStream

Modifier and Type	Method and Description
static ErrorStream	Main.getError() Get error stream for printing error messages.

Uses of ErrorStream in fmrisc.ProgramExplorer.InOut

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

Modifier and Type	Method and Description
static PackageSymbol	Package.construct(java.io.File[] dirs, ErrorStream error, java.io.File wdir) Create a package handler.
static Source	Source.create(java.io.File file, ErrorStream error) Construct a source file.
static java.io.File	Directory.setup(java.io.File parent, ErrorStream error) Set up task task directory in denoted parent directory.

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

Constructor and Description
ClassReader(Source source, ErrorStream error) Create a reader of a class declaration.
TheoryReader(Source source, ErrorStream error) Create a reader of a class declaration.

Uses of ErrorStream in fmrisc.ProgramExplorer.Judgements

Constructors in fmrisc.ProgramExplorer.Judgements with parameters of type ErrorStream

Constructor and Description
Satisfies(ParamSymbol method, StateType stype, TaskFolder invariants, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, ErrorStream out) Create a judgement processor.
Terminates(ParamSymbol method, StateType stype, TaskFolder tasks, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, ErrorStream out) Create a termination judgement processor.

Uses of ErrorStream in fmrisc.ProgramExplorer.Parser

Constructors in fmrisc.ProgramExplorer.Parser with parameters of type ErrorStream

Constructor and Description
MiniJavaLexer(org.antlr.runtime.CharStream input, ErrorStream error, Source source)
MiniJavaParser(org.antlr.runtime.TokenStream input, ErrorStream error, Source source)
SpecLangLexer(org.antlr.runtime.CharStream input, ErrorStream error, Source source)
SpecLangLexer(org.antlr.runtime.CharStream input, ErrorStream error, SourcePosition pos)
SpecLangParser(org.antlr.runtime.TokenStream input, ErrorStream error, Source source)
SpecLangParser(org.antlr.runtime.TokenStream input, ErrorStream error, SourcePosition pos, java.lang.String text)

Uses of ErrorStream in fmrisc.ProgramExplorer.Proving

Methods in fmrisc.ProgramExplorer.Proving with parameters of type ErrorStream

Modifier and Type	Method and Description
static ProofNavigatorProblem	ProofNavigator.translate(ClassicalProblem task, java.io.File dir, ErrorStream out) Translate classical problem to RISC ProofNavigator Problem

Constructors in fmrisc.ProgramExplorer.Proving with parameters of type ErrorStream

Constructor and Description
ClassicalProblem(Declaration[] decls, Formula goal, ErrorStream out) Construct a proving problem.
ProofNavigatorProblem(Declaration[] decls, Expression goal, java.io.File dir, ErrorStream out) Construct a proving problem from declarations and goal.
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 ErrorStream in fmrisc.ProgramExplorer.Semantics

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

Modifier and Type	Method and Description
static ConstructorSymbol	ConstructorSymbol.construct(ClassSymbol csymbol, Identifier name, Parameter[] params, TypeExpression[] atypes, ConstructorDeclaration decl, ErrorStream error) Construct class method symbol from declaration (NULL in case of error).
static ClassMethodSymbol	ClassMethodSymbol.construct(ClassSymbol csymbol, Identifier name, Parameter[] params, TypeExpression[] atypes, TypeExpression rtype, ClassMethodDeclaration decl, ErrorStream error) Construct class method symbol from declaration (NULL, in case of error).
static ObjectMethodSymbol	ObjectMethodSymbol.construct(ClassSymbol csymbol, Identifier name, Parameter[] params, TypeExpression[] atypes, TypeExpression rtype, ObjectMethodDeclaration decl, ErrorStream error) Construct object method symbol from declaration (NULL, in case of error).
static LogicChecking	LogicChecking.createChecker(ClassSymbol csymbol, Environment penv, ErrorStream error) Create checker for processing logical entities in environment set up by the (already processed) local theory of a class.
static LogicChecking	LogicChecking.createChecker(ErrorStream error) Create checker for processing logical entities in empty environment.
TheorySymbol	ClassSymbol.getClassTheory(ErrorStream error) Get theory symbol holding the logical type declaration for this class.
void	TypeTranslator.init(PackageSymbol top, ErrorStream error) Initialize type translator (which creates a base theory).
static boolean	Checking.process(ClassSymbol csymbol, ErrorStream error) Process the class symbol i.e.
static boolean	LogicChecking.process(TheorySymbol tsymbol, ErrorStream error) Process the theory symbol i.e.
boolean	TheorySymbol.read(ErrorStream error) Update declaration from reader or derive it from class symbol.
boolean	ClassSymbol.read(ErrorStream error) Update declaration from reader.
void	TheorySymbol.setDeclaration(TheoryDeclaration decl, ErrorStream error) Set and process new theory declaration

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

Constructor and Description
Environment(PackageSymbol top, ErrorStream error) Create a new environment at top-level.
LogicEnvironment(ErrorStream error) Create a new and empty environment.
LogicEnvironment(PackageSymbol top, ErrorStream error) Create a new environment at top-level.
LogicEnvironment(TheorySymbol tsymbol, ErrorStream error) Create a new environment from theory symbol.
LogicTypeTable(ErrorStream error) Construct a table for making types unique.
PackageSymbol(Identifier name, ErrorStream error, java.io.File dir) Construct symbol for top-level package.
PackageSymbol(PackageSymbol parent, Identifier name, ErrorStream error) Construct symbol for subpackage of another package.
ParamSymbols(ErrorStream error) Construct symbol table with denoted error stream.
ParamSymbolTable(ErrorStream error) Construct symbol table with denoted error stream.
SymbolTable(ErrorStream error) Construct symbol table with denoted error stream.
TCCGenerator(TheorySymbol tsymbol, java.util.Vector<TheorySymbol> theories, LogicEnvironment env, java.io.File parent, ErrorStream out) Construct a type checking condition generator.
TheorySymbol(ClassSymbol csymbol, Identifier name, TheoryDeclaration decl, ErrorStream error) Construct local theory symbol from declaration.
TheorySymbol(PackageSymbol psymbol, Identifier name, TheoryDeclaration decl, ErrorStream error) Construct theory symbol from declaration.

Uses of ErrorStream in fmrisc.ProgramExplorer.Syntax.Spec

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

Modifier and Type	Method and Description
static UnitSpec	UnitSpec.construct(java.lang.String text, ErrorStream error, SourcePosition pos) Construct unit specification from denoted text.
static ClassSpec	ClassSpec.construct(java.lang.String text, ErrorStream error, SourcePosition pos) Construct class specification from denoted text.
static StatementSpec	StatementSpec.construct(java.lang.String text, ErrorStream error, SourcePosition pos) Construct method specification from denoted text.
static LoopSpec	LoopSpec.construct(java.lang.String text, ErrorStream error, SourcePosition pos) Construct loop specification from denoted text.
static MethodSpec	MethodSpec.construct(java.lang.String text, ErrorStream error, SourcePosition pos) Construct method specification from denoted text.

Uses of ErrorStream in fmrisc.ProgramExplorer.Tasks

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

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	ClassTasks.register(ClassSymbol csymbol, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, ErrorStream out) Register the construction of tasks for a given class.
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.

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

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.
FormulaTask(FormulaDefinition formula, TheorySymbol theory, java.io.File parent, ErrorStream out) Construct a task.
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.
SpecTask(ParamSymbol method, boolean satisfiable, StateType stateType, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, ErrorStream out) Construct a task for validating a specification.
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.
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.