fmrisc.ProgramExplorer.Proving

Class ProofNavigatorProblem

java.lang.Object

fmrisc.ProgramExplorer.Proving.ProofNavigatorProblem

public final class ProofNavigatorProblem
extends java.lang.Object

A proving problem for the RISC ProofNavigator.

Constructor Summary

Constructors

Constructor and Description
ProofNavigatorProblem(Declaration[] decls, Expression goal, java.io.File dir, ErrorStream out) Construct a proving problem from declarations and goal.

Method Summary

Methods

Modifier and Type	Method and Description
static void	closeProof() Closes any pending proof.
boolean	existsProof() Determine whether there exists a (possibly incomplete or invalidated) proof for this problem in the store.
static boolean	existsProof(java.io.File dir) Determine whether there exists a (possibly incomplete or invalidated) proof for this problem in the store denoted by dir.
Proof	getProof() Get current proof, possibly load it from file.
boolean	isSolved() Determine whether problem is solved.
boolean	isUnsolvable() Determine whether problem is not solvable.
void	print(java.io.PrintWriter out) Print the problem.
static void	proofDone(Proof proof) Called if a proof is completed by the ProofNavigator.
void	proveAuto(Task task) Attempt to prove goal automatically.
void	proveManual(Task task) Start/resume manual proof.
void	proveStrategy(Task task) Attempt pseudo-interactive proof with automatic strategy

Methods inherited from class java.lang.Object

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

Constructor Detail

ProofNavigatorProblem

public ProofNavigatorProblem(Declaration[] decls,
                     Expression goal,
                     java.io.File dir,
                     ErrorStream out)

Construct a proving problem from declarations and goal.

Parameters:

decls - the declarations.

goal - the goal to be proved in the context of the declarations.

out - stream for printing messages

dir - the directory to be used for persistent data.

Method Detail

existsProof

public static boolean existsProof(java.io.File dir)

Determine whether there exists a (possibly incomplete or invalidated) proof for this problem in the store denoted by dir.

Parameters:

dir - the directory for the proof.

Returns:

true if a proof exists.

existsProof

public boolean existsProof()

Determine whether there exists a (possibly incomplete or invalidated) proof for this problem in the store.

Returns:

true if a proof exists.

isSolved

public boolean isSolved()

Determine whether problem is solved.

Returns:

true if and only if problem. is solved.

isUnsolvable

public boolean isUnsolvable()

Determine whether problem is not solvable.

Returns:

true if and only if problem cannot be solved.

print

public void print(java.io.PrintWriter out)

Print the problem.

Parameters:

out - the stream on which the task is to be printed.

proveAuto

public void proveAuto(Task task)

Attempt to prove goal automatically.

Parameters:

task - the associated task

proveStrategy

public void proveStrategy(Task task)

Attempt pseudo-interactive proof with automatic strategy

Parameters:

task - the associated task

proveManual

public void proveManual(Task task)

Start/resume manual proof.

Parameters:

task - the associated task

proofDone

public static void proofDone(Proof proof)

Called if a proof is completed by the ProofNavigator.

Parameters:

proof - the completed proof.

closeProof

public static void closeProof()

Closes any pending proof.

getProof

public Proof getProof()

Get current proof, possibly load it from file.

Returns:

proof the current proof (may be null).