fmrisc.ProgramExplorer.Proving

Class StateProblem

java.lang.Object

fmrisc.ProgramExplorer.Proving.StateProblem

public final class StateProblem
extends java.lang.Object

A proving problem in state logic.

Constructor Summary

Constructors

Constructor and Description
StateProblem(Declaration[] decls, Formula goal, java.util.Map<Symbol,Symbol> map, StateType stateType, Type stringType, java.util.Collection<VariableSymbol> variables, java.util.Collection<ClassSymbol> exceptions, ErrorStream out) Construct a proving problem.

Method Summary

Methods

Modifier and Type	Method and Description
ClassicalProblem	classicalProblem() Translate the task into a predicate logic proving task.
void	print(java.io.PrintWriter out) Print task to output stream.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

StateProblem

public StateProblem(Declaration[] decls,
            Formula goal,
            java.util.Map<Symbol,Symbol> map,
            StateType stateType,
            Type stringType,
            java.util.Collection<VariableSymbol> variables,
            java.util.Collection<ClassSymbol> exceptions,
            ErrorStream out)

Construct a proving problem.

Parameters:

decls - the declarations of entities referenced in the goal.

goal - the goal to be proved.

map - a map of type symbols to new type symbols

stateType - the current state type (null, if no state)

stringType - the string type

variables - the modifiable variables

exceptions - the throwable exceptions

out - a stream for printing messages

Method Detail

print

public void print(java.io.PrintWriter out)

Print task to output stream.

Parameters:

out - the stream to print to

classicalProblem

public ClassicalProblem classicalProblem()

Translate the task into a predicate logic proving task.

Returns:

the corresponding predicate logic task.