Package fmrisc.ProgramExplorer.Tasks

Interface Summary

Interface	Description
ClassicalTask	A task that can be translated to a classical proving problem.
ProofNavigatorTask	A task that is suitable for solving with the RISC ProofNavigator.
StateTask	A task that can be translated to a state proving problem.
Strategy	A strategy for solving a task.
Task	The interface to a verification task.
Task.Observer	A task observer.

Class Summary

Class	Description
AllNewStrategy	A strategy for folders that resumes all new tasks in folder.
AutoStrategy	A strategy that attempts automatic before interactive proving.
ClassicalTaskBase	Base of a task that can be translated to a classical proving problem.
ClassTasks	The delayed generation of method-related tasks.
CorrectnessTask	The task of proving the partial correctness of a method/constructor.
FailedTask	An unconditionally failed task.
FlattenDeclarations	Flatten nested declarations of a task.
FlattenDeclarations.Result	The flattening result.
FormulaTask	The task of proving a user-defined formula.
FrameTask	The task of checking the frame condition
InvariantTask	The task of proving the correctness of a loop invariant.
ManualStrategy	A strategy that attempts interactive proving.
MethodTasks	The delayed generation of method-related tasks.
PreconditionTasks	The tasks of proving that the preconditions of a method body are satisfied.
ProofNavigatorTaskBase	The base of a task suitable for solving with the RISC ProofNavigator.
SpecTask	A task for validating a specification
StateTaskBase	Base of a task that can be translated to a state proving problem.
TaskBase	The base class of a verification task
TaskFolder	A folder of verification tasks.
TerminationTask	The task of proving the termination of a statement.
TerminationTasks	The tasks of proving that a method is well-behaved with respect to termination.
TypeCheckingTask	The task of proving a type-checking condition.

Enum Summary

Enum	Description
Task.Status	A task status.