fmrisc.ProgramExplorer.Tasks

Class StateTaskBase

java.lang.Object

fmrisc.ProgramExplorer.Tasks.TaskBase

fmrisc.ProgramExplorer.Tasks.ProofNavigatorTaskBase

fmrisc.ProgramExplorer.Tasks.ClassicalTaskBase

fmrisc.ProgramExplorer.Tasks.StateTaskBase

All Implemented Interfaces:

ClassicalTask, ProofNavigatorTask, StateTask, Task

Direct Known Subclasses:

CorrectnessTask, InvariantTask, SpecTask, TerminationTask, TypeCheckingTask

public abstract class StateTaskBase
extends ClassicalTaskBase
implements StateTask

Base of a task that can be translated to a state proving problem.

Nested Class Summary

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

Task.Observer, Task.Status

Method Summary

Modifier and Type	Method and Description
ClassicalProblem	classicalProblem() Translate task into a proving problem in classical logic.

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, print, resume, resumeOnNew, 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.StateTask

stateProblem

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, print, resume, resumeOnNew, setObserver, setParent, setStatus

Method Detail

classicalProblem

public ClassicalProblem classicalProblem()

Translate task into a proving problem in classical logic.

Specified by:

classicalProblem in interface ClassicalTask

Returns:

the translation result