public class InvariantTask extends StateTaskBase
Task.Observer, Task.Status
Constructor and Description |
---|
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.
|
Modifier and Type | Method and Description |
---|---|
void |
print(java.io.PrintWriter out)
Print linear representation of task.
|
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, resumeOnNew, setDirectory, setObserver, setStatus
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
proofNavigatorProblem, reset
getDirectory, getEvidence, getInfo, getName, getParent, getPosition, getStatus, isFinal, isOptional, resume, resumeOnNew, setObserver, setParent, setStatus
public 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)
method
- the method in which the invariant arises.stat
- the loop in which the invariant arises.goal
- the goal to be proved (constructed outside)invariant
- the invariant.pos
- the position of the corresponding loopcond
- the loop condition.body
- the specification of the loop body.parent
- the parent file.stateType
- 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 void print(java.io.PrintWriter out)
public StateProblem stateProblem()