fmrisc.ProgramExplorer.Tasks

Class TypeCheckingTask

java.lang.Object

fmrisc.ProgramExplorer.Tasks.TaskBase

fmrisc.ProgramExplorer.Tasks.ProofNavigatorTaskBase

fmrisc.ProgramExplorer.Tasks.ClassicalTaskBase

fmrisc.ProgramExplorer.Tasks.StateTaskBase

fmrisc.ProgramExplorer.Tasks.TypeCheckingTask

All Implemented Interfaces:

ClassicalTask, ProofNavigatorTask, StateTask, Task

public class TypeCheckingTask
extends StateTaskBase

The task of proving a type-checking condition.

Nested Class Summary

Nested classes/interfaces inherited from interface fmrisc.ProgramExplorer.Tasks.Task

Task.Observer, Task.Status

Constructor Summary

Constructors

Constructor and Description
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.

Method Summary

Methods

Modifier and Type	Method and Description
void	print(java.io.PrintWriter out) Print linear representation of task.
boolean	resumeOnNew() Determine whether new task is to be resumed.
StateProblem	stateProblem() Translate task into a proving problem in state logic.

Methods inherited from class fmrisc.ProgramExplorer.Tasks.StateTaskBase

classicalProblem

Methods inherited from class fmrisc.ProgramExplorer.Tasks.ClassicalTaskBase

proofNavigatorProblem, reset

Methods inherited from class fmrisc.ProgramExplorer.Tasks.ProofNavigatorTaskBase

setParent

Methods inherited from class fmrisc.ProgramExplorer.Tasks.TaskBase

getDirectory, getEvidence, getInfo, getName, getParent, getParentDirectory, getPosition, getStatus, isFinal, isOptional, resume, setDirectory, setObserver, setStatus

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface fmrisc.ProgramExplorer.Tasks.ProofNavigatorTask

proofNavigatorProblem, reset

Methods inherited from interface fmrisc.ProgramExplorer.Tasks.Task

getDirectory, getEvidence, getInfo, getName, getParent, getPosition, getStatus, isFinal, isOptional, resume, setObserver, setParent, setStatus

Constructor Detail

TypeCheckingTask

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

Parameters:

tsymbol - the theory of the task.

name - the name of the task.

position - a related source position (may be null)

dir - a directory for writing persistent information

resultType - the type of the current state (null, if none)

stateVars - the names of the modifiable variables (null, if none)

stateExcs - the names of the throwable exceptions (null, if none)

theories - a vector of theories on which the following depend.

decls - a sequence of declaration lists.

goal - the goal to be proved.

out - the stream to which to write error messages.

Method Detail

resumeOnNew

public boolean resumeOnNew()

Determine whether new task is to be resumed.

Specified by:

resumeOnNew in interface Task

Overrides:

resumeOnNew in class TaskBase

Returns:

true if new task is to be resumed.

print

public void print(java.io.PrintWriter out)

Print linear representation of task.

Specified by:

print in interface Task

Overrides:

print in class TaskBase

Parameters:

out - the stream to write to.

stateProblem

public StateProblem stateProblem()

Translate task into a proving problem in state logic.

Returns:

the translation result