jml2b.pog.lemma
Class GoalStatus

java.lang.Object
  jml2b.util.Profiler
      jml2b.pog.lemma.GoalStatus

public class GoalStatus

extends Profiler

This class provides constants and facilities to manage the status of a goal.

Author:

L. Burdy

Constructor Summary

GoalStatus()
Constructs by default a goal status.

GoalStatus(JpoInputStream s)
Constructs a non obvious goal from a .jpo file

Method Summary

ProverStatus	getProverStatus(java.lang.String name) Returns the prove force.
boolean	isChecked() Tests whether the goal is checked or not.
boolean	isProved()
boolean	isProved(java.lang.String prover)
void	save(JpoOutputStream s) Saves the goal status in the a .jpo file
void	setChecked() Sets the proof state to CHECKED.
void	setProved(int prover) Sets the proof state to PROVED.
void	setStatus(java.lang.String prover, ProverStatus ps)
void	setUnproved() Sets the proof state to UNPROVED.

Methods inherited from class jml2b.util.Profiler

runGC

Methods inherited from class java.lang.Object

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

Constructor Detail

GoalStatus

public GoalStatus()

Constructs by default a goal status. The state will be UNPROVED.

GoalStatus

public GoalStatus(JpoInputStream s)
           throws java.io.IOException,
                  LoadException

Constructs a non obvious goal from a .jpo file

Throws:

IOEXception

LoadException

java.io.IOException

Method Detail

setProved

public void setProved(int prover)

Sets the proof state to PROVED.

setChecked

public void setChecked()

Sets the proof state to CHECKED.

setUnproved

public void setUnproved()

Sets the proof state to UNPROVED.

isProved

public boolean isProved(java.lang.String prover)

isProved

public boolean isProved()

isChecked

public boolean isChecked()

Tests whether the goal is checked or not.

Returns:

true if the proof state is CHECKED, false otherwise

save

public 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)

getProverStatus

public ProverStatus getProverStatus(java.lang.String name)

Returns the prove force.

Returns:

proveForce

setStatus

public void setStatus(java.lang.String prover,
                      ProverStatus ps)