public final class TerminationTask extends StateTaskBase
Task.Observer, Task.Status
Constructor and Description |
---|
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.
|
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 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)
kind
- a description of the kind of the task.method
- the method in which the task arises.goal
- the goal to be proved (constructed outside)stat
- the statement whose termination is proved (may be null)tag
- the tag to use for the task if statement is nullparent
- the parent filestateType
- the type of the current state (null, if none)variables
- the names of the variables modified in the loop body.exceptions
- the names of the exceptions thrown in the loop body.theories
- the theories on which the following depend in dependence order.decls
- a sequence of declaration lists.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()