public class TypeCheckingTask extends StateTaskBase
Task.Observer, Task.Status
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.
|
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.
|
classicalProblem
proofNavigatorProblem, reset
setParent
getDirectory, getEvidence, getInfo, getName, getParent, getParentDirectory, getPosition, getStatus, isFinal, isOptional, resume, setDirectory, setObserver, setStatus
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
proofNavigatorProblem, reset
getDirectory, getEvidence, getInfo, getName, getParent, getPosition, getStatus, isFinal, isOptional, resume, setObserver, setParent, setStatus
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)
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 informationresultType
- 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.public boolean resumeOnNew()
resumeOnNew
in interface Task
resumeOnNew
in class TaskBase
public void print(java.io.PrintWriter out)
public StateProblem stateProblem()