jack.plugin.prove
Class ProofTask

java.lang.Object
  java.lang.Thread
      jack.plugin.prove.ProofTask

All Implemented Interfaces:

java.lang.Runnable

public abstract class ProofTask

extends java.lang.Thread

Class corresponding to a proof task that must be (or is) performed.

Author:

A. Requet, L. Burdy

Field Summary

static int	ERROR Constant corresponding to the error state.
static int	FINISHED Constant corresponding to the state.
static int	LOADING Constant corresponding to the loading state.
static int	RUNNING Constant corresponding to the running state.
static int	STARTING Constant corresponding to the starting state.
static int	STOPPED
static int	WAITING Constant corresponding to the waiting state.

Fields inherited from class java.lang.Thread

MAX_PRIORITY, MIN_PRIORITY, NORM_PRIORITY

Constructor Summary

ProofTask()

ProofTask(ICaseExplorer c)

Method Summary

abstract ProveAction	factory()
abstract ProofTask	factory(org.eclipse.core.resources.IFile jpoFile, org.eclipse.jdt.core.ICompilationUnit cu)
java.util.Date	getCreationDate() Return the creation date of the task.
java.util.Date	getEndDate() Returns the end date of the task.
java.lang.String	getErrorDescription() Returns the description of the last error encountered.
java.lang.String	getErrorDetails() Returns detail about the last error encountered.
java.lang.String	getFileName()
int	getNumPos()
int	getNumToTry() Returns the number of proof obligations that still have to be tried.
int	getPoProved() Returns the number of proved proof obligations.
int	getPoTried() Returns the number of proof obligations that have already been tried.
abstract java.lang.String	getProverName() return the name of the prover used by this ProofTask.
java.util.Date	getStartDate() Return the start date of teh task.
int	getState() Returns the state of the task.
java.lang.String	getStringState()
boolean	isRunning() Returns true iff proofs are currently performed on this task.
int	nbPo() Returns the total number of proof obligations.
abstract void	run() Starts the proof.
void	setEndOp(TreeItemSelection ehl)
void	setJPov(JpoFile jpoFile2)
void	setPartial(java.lang.String repos) This method is called when the partial mode is called.
void	start()
void	stopAsSoonAsYouCanPlease() Function that asks the thread to stop when he can.

Methods inherited from class java.lang.Thread

activeCount, checkAccess, countStackFrames, currentThread, destroy, dumpStack, enumerate, getContextClassLoader, getName, getPriority, getThreadGroup, holdsLock, interrupt, interrupted, isAlive, isDaemon, isInterrupted, join, join, join, resume, setContextClassLoader, setDaemon, setName, setPriority, sleep, sleep, stop, stop, suspend, toString, yield

Methods inherited from class java.lang.Object

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

Field Detail

FINISHED

public static final int FINISHED

Constant corresponding to the state. That is when the proof has either terminited normally, or been aborted.

See Also:

Constant Field Values

WAITING

public static final int WAITING

Constant corresponding to the waiting state. That is, when the task has not been started yet, and is waiting that another task finishes for starting.

See Also:

Constant Field Values

RUNNING

public static final int RUNNING

Constant corresponding to the running state. That is, when the proof is currently running.

See Also:

Constant Field Values

LOADING

public static final int LOADING

Constant corresponding to the loading state. That is, when the task is loading the list of proof obligations.

See Also:

Constant Field Values

STARTING

public static final int STARTING

Constant corresponding to the starting state. That is, when the task has been selected for run but has not begin running yet.

See Also:

Constant Field Values

STOPPED

public static final int STOPPED

See Also:

Constant Field Values

ERROR

public static final int ERROR

Constant corresponding to the error state. That is, when the task has stopped due to an error.

See Also:

Constant Field Values

Constructor Detail

ProofTask

public ProofTask()

ProofTask

public ProofTask(ICaseExplorer c)

Parameters:

c -

Method Detail

isRunning

public boolean isRunning()

Returns true iff proofs are currently performed on this task.

factory

public abstract ProofTask factory(org.eclipse.core.resources.IFile jpoFile,
                                  org.eclipse.jdt.core.ICompilationUnit cu)

factory

public abstract ProveAction factory()

getState

public int getState()

Returns the state of the task. The returned state can be one of:

• RUNNING,
• FINISHED,
• LOADING,
• WAITING or
• ERROR

getStringState

public java.lang.String getStringState()

getFileName

public java.lang.String getFileName()

stopAsSoonAsYouCanPlease

public void stopAsSoonAsYouCanPlease()

Function that asks the thread to stop when he can.

getPoTried

public int getPoTried()

Returns the number of proof obligations that have already been tried.

Returns:

the number of proof obligations already tried.

getNumToTry

public int getNumToTry()

Returns the number of proof obligations that still have to be tried.

Returns:

the number of proof obligations that still have to be tried.

getPoProved

public int getPoProved()

Returns the number of proved proof obligations.

Returns:

the number of proved proof obligations.

getCreationDate

public java.util.Date getCreationDate()

Return the creation date of the task.

Returns:

the creation date of the task.

getStartDate

public java.util.Date getStartDate()

Return the start date of teh task. That is the time where the proof started.

Returns:

the start date of the task.

getEndDate

public java.util.Date getEndDate()

Returns the end date of the task.

Returns:

the end date fo the task.

nbPo

public int nbPo()

Returns the total number of proof obligations.

Returns:

the total number of proof obligations.

getErrorDescription

public java.lang.String getErrorDescription()

Returns the description of the last error encountered.

This method will only provide meaningfull values if the current state is ERROR.

Returns:

the description of the last error encountered, if any.

getErrorDetails

public java.lang.String getErrorDetails()

Returns detail about the last error encountered.

In case were no details are available, returns null.

Returns:

detailed information on the last error encountered, null in case where no information is available.

run

public abstract void run()

Starts the proof.

start

public void start()

getProverName

public abstract java.lang.String getProverName()

return the name of the prover used by this ProofTask.

getNumPos

public int getNumPos()

Returns:

setJPov

public void setJPov(JpoFile jpoFile2)

Parameters:

jpoFile2 -

setEndOp

public void setEndOp(TreeItemSelection ehl)

Parameters:

ehl -

setPartial

public void setPartial(java.lang.String repos)

This method is called when the partial mode is called.