fmrisc.ProgramExplorer.Tasks

Class InvariantTask

java.lang.Object

fmrisc.ProgramExplorer.Tasks.TaskBase

fmrisc.ProgramExplorer.Tasks.ProofNavigatorTaskBase

fmrisc.ProgramExplorer.Tasks.ClassicalTaskBase

fmrisc.ProgramExplorer.Tasks.StateTaskBase

fmrisc.ProgramExplorer.Tasks.InvariantTask

All Implemented Interfaces:

ClassicalTask, ProofNavigatorTask, StateTask, Task

public class InvariantTask
extends StateTaskBase

The task of proving the correctness of a loop invariant.

Nested Class Summary

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

Task.Observer, Task.Status

Constructor Summary

Constructors

Constructor and Description
InvariantTask(ParamSymbol method, Statement stat, Formula goal, Formula invariant, SourcePosition pos, Formula cond, Formula body, java.io.File parent, StateType stateType, java.util.Set<VariableSymbol> variables, java.util.Set<ClassSymbol> exceptions, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, ErrorStream out) Construct an invariant verification task.

Method Summary

Methods

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

InvariantTask

public InvariantTask(ParamSymbol method,
             Statement stat,
             Formula goal,
             Formula invariant,
             SourcePosition pos,
             Formula cond,
             Formula body,
             java.io.File parent,
             StateType stateType,
             java.util.Set<VariableSymbol> variables,
             java.util.Set<ClassSymbol> exceptions,
             java.util.Vector<TheorySymbol> theories,
             Declaration[][] decls,
             ErrorStream out)

Construct an invariant verification task.

Parameters:

method - the method in which the invariant arises.

stat - the loop in which the invariant arises.

goal - the goal to be proved (constructed outside)

invariant - the invariant.

pos - the position of the corresponding loop

cond - the loop condition.

body - the specification of the loop body.

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

variables - the names of the variables modified in the loop body.

exceptions - the names of the exceptions thrown in the loop body.

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