fmrisc.ProgramExplorer.Tasks

Class TerminationTask

java.lang.Object

fmrisc.ProgramExplorer.Tasks.TaskBase

fmrisc.ProgramExplorer.Tasks.ProofNavigatorTaskBase

fmrisc.ProgramExplorer.Tasks.ClassicalTaskBase

fmrisc.ProgramExplorer.Tasks.StateTaskBase

fmrisc.ProgramExplorer.Tasks.TerminationTask

All Implemented Interfaces:

ClassicalTask, ProofNavigatorTask, StateTask, Task

public final class TerminationTask
extends StateTaskBase

The task of proving the termination of a statement.

Nested Class Summary

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

Task.Observer, Task.Status

Constructor Summary

Constructors

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.

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

TerminationTask

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)

Construct a termination verification task.

Parameters:

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 null

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.

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