fmrisc.ProgramExplorer.Tasks

Class SpecTask

java.lang.Object

fmrisc.ProgramExplorer.Tasks.TaskBase

fmrisc.ProgramExplorer.Tasks.ProofNavigatorTaskBase

fmrisc.ProgramExplorer.Tasks.ClassicalTaskBase

fmrisc.ProgramExplorer.Tasks.StateTaskBase

fmrisc.ProgramExplorer.Tasks.SpecTask

All Implemented Interfaces:

ClassicalTask, ProofNavigatorTask, StateTask, Task

public final class SpecTask
extends StateTaskBase

A task for validating a specification

Nested Class Summary

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

Task.Observer, Task.Status

Constructor Summary

Constructors

Constructor and Description
SpecTask(ParamSymbol method, boolean satisfiable, StateType stateType, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, ErrorStream out) Construct a task for validating a specification.

Method Summary

Modifier and Type	Method and Description
StateProblem	stateProblem() Construct a state problem from the task.

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, print, 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, print, resume, resumeOnNew, setObserver, setParent, setStatus

Constructor Detail

SpecTask

public SpecTask(ParamSymbol method,
                boolean satisfiable,
                StateType stateType,
                java.util.Vector<TheorySymbol> theories,
                Declaration[][] decls,
                ErrorStream out)

Construct a task for validating a specification.

Parameters:

method - the method whose specification is to be validated

satisfiable - if true, the specification is checked for satisfiablility. if false, it is checked for non-triviality (tautology)

stateType - the type of the current state (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

stateProblem

public StateProblem stateProblem()

Construct a state problem from the task.

Returns:

the translation.