fmrisc.ProgramExplorer.Tasks

Class CorrectnessTask

java.lang.Object

fmrisc.ProgramExplorer.Tasks.TaskBase

fmrisc.ProgramExplorer.Tasks.ProofNavigatorTaskBase

fmrisc.ProgramExplorer.Tasks.ClassicalTaskBase

fmrisc.ProgramExplorer.Tasks.StateTaskBase

fmrisc.ProgramExplorer.Tasks.CorrectnessTask

All Implemented Interfaces:

ClassicalTask, ProofNavigatorTask, StateTask, Task

public class CorrectnessTask
extends StateTaskBase

The task of proving the partial correctness of a method/constructor.

Nested Class Summary

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

Task.Observer, Task.Status

Constructor Summary

Constructors

Constructor and Description
CorrectnessTask(ParamSymbol method, java.io.File parent, StateType stateType, Name[] stateVars, Name[] stateExcs, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, ErrorStream out) Construct a partial correctness task for a given method.

Method Summary

Modifier and Type	Method and Description
void	print(java.io.PrintWriter out) Print linear representation of task.
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, 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.ProofNavigatorTask

proofNavigatorProblem, reset

Methods inherited from interface fmrisc.ProgramExplorer.Tasks.Task

getDirectory, getEvidence, getInfo, getName, getParent, getPosition, getStatus, isFinal, isOptional, resume, resumeOnNew, setObserver, setParent, setStatus

Constructor Detail

CorrectnessTask

public CorrectnessTask(ParamSymbol method,
                       java.io.File parent,
                       StateType stateType,
                       Name[] stateVars,
                       Name[] stateExcs,
                       java.util.Vector<TheorySymbol> theories,
                       Declaration[][] decls,
                       ErrorStream out)

Construct a partial correctness task for a given method.

Parameters:

method - the symbol of a method with a specification.

parent - the parent of the new directory for this task

stateType - the type of the current state (null, if none)

stateVars - the names of the modifiable variables (null, if none)

stateExcs - the names of the throwable exceptions (null, if none)

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

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