Uses of Interface
fmrisc.ProgramExplorer.Tasks.Task

Packages that use Task

Package	Description
fmrisc.ProgramExplorer
fmrisc.ProgramExplorer.Proving
fmrisc.ProgramExplorer.SWT
fmrisc.ProgramExplorer.Tasks

Uses of Task in fmrisc.ProgramExplorer

Methods in fmrisc.ProgramExplorer with parameters of type Task

Modifier and Type	Method and Description
static void	Main.displayInfo(Task task) Display info (proof) associated to task.

Uses of Task in fmrisc.ProgramExplorer.Proving

Methods in fmrisc.ProgramExplorer.Proving with parameters of type Task

Modifier and Type	Method and Description
void	ProofNavigatorProblem.proveAuto(Task task) Attempt to prove goal automatically.
void	ProofNavigatorProblem.proveManual(Task task) Start/resume manual proof.
void	ProofNavigatorProblem.proveStrategy(Task task) Attempt pseudo-interactive proof with automatic strategy

Uses of Task in fmrisc.ProgramExplorer.SWT

Methods in fmrisc.ProgramExplorer.SWT with parameters of type Task

Modifier and Type	Method and Description
void	TopWindow.redraw(org.eclipse.swt.widgets.TreeItem node, Task task, boolean color) Redraw node to indicate status of task.

Uses of Task in fmrisc.ProgramExplorer.Tasks

Subinterfaces of Task in fmrisc.ProgramExplorer.Tasks

Modifier and Type	Interface and Description
interface	ClassicalTask A task that can be translated to a classical proving problem.
interface	ProofNavigatorTask A task that is suitable for solving with the RISC ProofNavigator.
interface	StateTask A task that can be translated to a state proving problem.

Classes in fmrisc.ProgramExplorer.Tasks that implement Task

Modifier and Type	Class and Description
class	ClassicalTaskBase Base of a task that can be translated to a classical proving problem.
class	CorrectnessTask The task of proving the partial correctness of a method/constructor.
class	FailedTask An unconditionally failed task.
class	FormulaTask The task of proving a user-defined formula.
class	FrameTask The task of checking the frame condition
class	InvariantTask The task of proving the correctness of a loop invariant.
class	ProofNavigatorTaskBase The base of a task suitable for solving with the RISC ProofNavigator.
class	SpecTask A task for validating a specification
class	StateTaskBase Base of a task that can be translated to a state proving problem.
class	TaskBase The base class of a verification task
class	TaskFolder A folder of verification tasks.
class	TerminationTask The task of proving the termination of a statement.
class	TypeCheckingTask The task of proving a type-checking condition.

Methods in fmrisc.ProgramExplorer.Tasks that return Task

Modifier and Type	Method and Description
Task[]	TaskFolder.getTasks() Get tasks appropriately sorted for display

Methods in fmrisc.ProgramExplorer.Tasks with parameters of type Task

Modifier and Type	Method and Description
void	TaskFolder.add(Task task) Add task to folder.
void	AllNewStrategy.apply(Task task) Apply this strategy to a task to which it is applicable.
void	AutoStrategy.apply(Task task) Apply this strategy to a task to which it is applicable.
void	ManualStrategy.apply(Task task) Apply this strategy to a task to which it is applicable.
void	Strategy.apply(Task task) Apply this strategy to a task to which it is applicable.
boolean	AllNewStrategy.isApplicable(Task task) True if this strategy is applicable to the denoted task.
boolean	AutoStrategy.isApplicable(Task task) True if this strategy is applicable to the denoted task.
boolean	ManualStrategy.isApplicable(Task task) True if this strategy is applicable to the denoted task.
boolean	Strategy.isApplicable(Task task) True if this strategy is applicable to the denoted task.
void	Task.Observer.sendNotification(Task task) Notify observer that the status of the denoted task has changed.