jml2b.pog.lemma
Class NonObviousGoal

java.lang.Object
  jml2b.util.Profiler
      jml2b.pog.lemma.Goal
          jml2b.pog.lemma.NonObviousGoal

All Implemented Interfaces:

IFormToken, ILemma, MyToken

public class NonObviousGoal

extends Goal

This class implements a non obvious goal, that is a goal that will be saved in the JPO file.

Author:

L. Burdy

Field Summary

Fields inherited from interface jml2b.structure.statement.MyToken

BTRUE, FIRST_TOKEN, METHOD_CALL, NEWARRAY, nodeString, SEQUENCE, SKIP, T_CALLED_OLD, T_FRESH_CALLED_OLD, T_VARIANT_OLD

Fields inherited from interface jml2b.formula.IFormToken

ARRAY_ACCESS, ARRAY_RANGE, B_ACCOLADE, B_APPLICATION, B_ARRAY_EQUALS, B_BOOL, B_BTRUE, B_COUPLE, B_DOM, B_FUNCTION_EQUALS, B_IN, B_INTERVAL, B_OVERRIDING, B_SET_EQUALS, B_SUBSTRACTION_DOM, B_UNION, CONSTANT_FUNCTION, CONSTANT_FUNCTION_FUNCTION, EQUALS_ON_OLD_INSTANCES, EQUALS_ON_OLD_INSTANCES_ARRAY, FINAL_IDENT, GUARDED_SET, INTERSECTION_IS_NOT_EMPTY, IS_ARRAY, IS_MEMBER_FIELD, IS_STATIC_FIELD, Ja_ADD_OP, Ja_AND_OP, Ja_CHAR_LITERAL, Ja_COMMA, Ja_DIFFERENT_OP, Ja_DIV_OP, Ja_EQUALS_OP, Ja_GE_OP, Ja_GREATER_OP, Ja_IDENT, Ja_JAVA_BUILTIN_TYPE, Ja_LE_OP, Ja_LESS_OP, Ja_LITERAL_false, Ja_LITERAL_null, Ja_LITERAL_super, Ja_LITERAL_this, Ja_LITERAL_true, Ja_LNOT, Ja_MOD, Ja_MUL_OP, Ja_NEGATIVE_OP, Ja_NUM_INT, Ja_OR_OP, Ja_QUESTION, Ja_STRING_LITERAL, Ja_UNARY_NUMERIC_OP, Jm_AND_THEN, Jm_EXISTS, Jm_FORALL, Jm_IMPLICATION_OP, Jm_IS_SUBTYPE, Jm_OR_ELSE, Jm_T_OLD, Jm_T_RESULT, Jm_T_TYPE, LOCAL_ELEMENTS_DECL, LOCAL_VAR_DECL, MODIFIED_FIELD, NEW_OBJECT, T_CALLED_OLD, T_TYPE, T_VARIANT_OLD, toString

Constructor Summary

NonObviousGoal()

NonObviousGoal(Goal g)
Constructs a non obvious goal from a goal with a goal status to unproved.

Method Summary

boolean	isChecked()
boolean	isProved() Returns whether this goal is proven.
boolean	isProved(java.lang.String prover) Returns whether this goal is proven.
void	mergeWith(Goal e) Compares the goal with a set of possible loaded goals.
void	save(IJml2bConfiguration config, JpoOutputStream s, JmlFile jf) Saves the goal in a .jpo file
int	setNumber(int i) Sets the goal number

Methods inherited from class jml2b.pog.lemma.Goal

addImplicToGoal, clone, garbageIdent, getFields, getFormula, getSubs, isOriginal, oldParam, proveObvious, setObvious, sub, suppressSpecialOld

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

NonObviousGoal

public NonObviousGoal()

NonObviousGoal

public NonObviousGoal(Goal g)

Constructs a non obvious goal from a goal with a goal status to unproved.

Parameters:

g - The goal

Method Detail

isProved

public boolean isProved(java.lang.String prover)

Returns whether this goal is proven.

Returns:

true if the goal is proved, false otherwise

isProved

public boolean isProved()

Returns whether this goal is proven.

Returns:

true if the goal is proved, false otherwise

isChecked

public boolean isChecked()

setNumber

public int setNumber(int i)

Sets the goal number

Parameters:

i - The goal number

mergeWith

public void mergeWith(Goal e)

Compares the goal with a set of possible loaded goals. If the goals merge, the goal state is updated with the loaded goal.

Parameters:

e - The set of loaded goals.

Throws:

MergeException

save

public void save(IJml2bConfiguration config,
                 JpoOutputStream s,
                 JmlFile jf)
          throws java.io.IOException

Saves the goal in a .jpo file

Parameters:

s - The ouput stream representing the jpo file.

jf - The current JML file

Throws:

java.io.IOException