Uses of Class
fmrisc.ProgramExplorer.Syntax.Logic.StateType

Packages that use StateType

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

Uses of StateType in fmrisc.ProgramExplorer.InOut

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

Modifier and Type	Method and Description
void	Breaks.visit(StateType exp)
void	PrettyPrinter.visit(StateType exp)
void	PrettyMathML.visit(StateType exp)

Uses of StateType in fmrisc.ProgramExplorer.Judgements

Methods in fmrisc.ProgramExplorer.Judgements that return StateType

Modifier and Type	Method and Description
StateType	Satisfies.getStateType() Get the state type of this judgement processor

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

Constructor and Description
Post(StateType stype) Create a judgement processor.
Pre(StateType stype) Create a judgement processor.
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 StateType in fmrisc.ProgramExplorer.Proving

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

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 StateType in fmrisc.ProgramExplorer.Semantics

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

Modifier and Type	Method and Description
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	LogicTypeTable.setStateContext(StateType stateType, Name[] stateVars, Name[] stateExcs) Set the current state context.

Uses of StateType in fmrisc.ProgramExplorer.Syntax

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

Modifier and Type	Method and Description
void	ASTVisitor.visit(StateType tree)
void	ASTPrinter.visit(StateType exp)
void	ASTCloner.visit(StateType tree)
void	ASTVisitorBase.visit(StateType tree)

Uses of StateType in fmrisc.ProgramExplorer.Syntax.Logic

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

Modifier and Type	Method and Description
static StateType	StateType.construct(Type ret) Construct a state type.

Uses of StateType in fmrisc.ProgramExplorer.Tasks

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

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	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 StateType

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.
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.