fmrisc.ProgramExplorer.Tasks

Interface Task

All Known Subinterfaces:

ClassicalTask, ProofNavigatorTask, StateTask

All Known Implementing Classes:

ClassicalTaskBase, CorrectnessTask, FailedTask, FormulaTask, FrameTask, InvariantTask, ProofNavigatorTaskBase, SpecTask, StateTaskBase, TaskBase, TaskFolder, TerminationTask, TypeCheckingTask

public interface Task

The interface to a verification task.

Nested Class Summary

Nested Classes

Modifier and Type	Interface and Description
static interface	Task.Observer A task observer.
static class	Task.Status A task status.

Method Summary

Modifier and Type	Method and Description
java.io.File	getDirectory() Get directory to be used for writing persistent data
java.lang.String	getEvidence() Get evidence for task status.
java.lang.Object	getInfo() Get additional information for task status.
java.lang.String	getName() Get the name of the task.
TaskFolder	getParent() Get folder containing current task.
SourcePosition	getPosition() Get source code position linked to this task (null, if none)
Task.Status	getStatus() Get status of task.
boolean	isFinal() Determine whether task status is final.
boolean	isOptional() Determine whether task is optional.
void	print(java.io.PrintWriter out) Print linear representation of task.
Task.Status	resume() Attempt to perform task which is in status NEW or OPEN.
boolean	resumeOnNew() Determine whether new task is to be resumed.
void	setObserver(Task.Observer observer) Set observer for this task.
void	setParent(TaskFolder parent) Set folder containing current task.
void	setStatus(Task.Status status, java.lang.String evidence, java.lang.Object info) Set task status.

Method Detail

getName

java.lang.String getName()

Get the name of the task.

Returns:

the task name.

resumeOnNew

boolean resumeOnNew()

Determine whether new task is to be resumed.

Returns:

true if new task is to be resumed.

isOptional

boolean isOptional()

Determine whether task is optional.

Returns:

true if task is optional.

getStatus

Task.Status getStatus()

Get status of task.

Returns:

the task status.

isFinal

boolean isFinal()

Determine whether task status is final.

Returns:

true iff task status is DONE or FAILED.

resume

Task.Status resume()

Attempt to perform task which is in status NEW or OPEN.

Returns:

the resulting task status (OPEN, DONE, or FAILED).

getPosition

SourcePosition getPosition()

Get source code position linked to this task (null, if none)

Returns:

the position.

setParent

void setParent(TaskFolder parent)

Set folder containing current task.

Parameters:

parent - the parent folder (may be null).

getParent

TaskFolder getParent()

Get folder containing current task.

Returns:

the parent folder (may be null).

getDirectory

java.io.File getDirectory()

Get directory to be used for writing persistent data

Returns:

the directory.

print

void print(java.io.PrintWriter out)

Print linear representation of task.

Parameters:

out - the writer.

setStatus

void setStatus(Task.Status status,
               java.lang.String evidence,
               java.lang.Object info)

Set task status.

Parameters:

status - the task status.

evidence - the evidence for the status (may be null).

info - additional information (may be null)

getEvidence

java.lang.String getEvidence()

Get evidence for task status.

Returns:

the evidence (may be null)

getInfo

java.lang.Object getInfo()

Get additional information for task status.

Returns:

the information (may be null)

setObserver

void setObserver(Task.Observer observer)

Set observer for this task.

Parameters:

observer - a task observer