jml2b.pog.lemma
Class ProverStatus

java.lang.Object
  jml2b.pog.lemma.ProverStatus

public abstract class ProverStatus

extends java.lang.Object

Author:

L. Burdy

Field Summary

static byte	PROVED Proof state value that corresponds to a goal that is proved.
static byte	UNPROVED Proof state value that corresponds to a goal that is not proved neither checked.

Constructor Summary

ProverStatus()

Method Summary

boolean	isProved() Tests whether the goal is proved or not
boolean	isUnproved() Tests whether the goal is unproved or not.
abstract void	save(JpoOutputStream s) Saves the goal status in the a .jpo file
void	setUnproved() Sets the proof state to UNPROVED.

Methods inherited from class java.lang.Object

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

Field Detail

UNPROVED

public static final byte UNPROVED

Proof state value that corresponds to a goal that is not proved neither checked.

See Also:

Constant Field Values

PROVED

public static final byte PROVED

Proof state value that corresponds to a goal that is proved.

See Also:

Constant Field Values

Constructor Detail

ProverStatus

public ProverStatus()

Method Detail

setUnproved

public void setUnproved()

Sets the proof state to UNPROVED.

isProved

public boolean isProved()

Tests whether the goal is proved or not

Returns:

true if the proof state is PROVED, false otherwise

isUnproved

public boolean isUnproved()

Tests whether the goal is unproved or not.

Returns:

true if the proof state is UNPROVED, false otherwise

save

public abstract void save(JpoOutputStream s)
                   throws java.io.IOException

Saves the goal status in the a .jpo file

Parameters:

s - The output stream for the jpo file

Throws:

java.io.IOException

See Also:

NonObviousGoal#save(DataOutputStream, JmlFile, IJmlFile)