jml2b.pog.lemma
Class Goal

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

All Implemented Interfaces:

IFormToken, ILemma, MyToken

Direct Known Subclasses:

NonObviousGoal

public class Goal

extends Profiler

implements MyToken, ILemma, IFormToken

This class implements a goal.

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

Goal(Formula f, GoalOrigin origin)
Constructs a goal from a formula and an origin.

Goal(VirtualFormula vf, GoalOrigin origin)
Constructs a goal from a formula and an origin.

Method Summary

void	addImplicToGoal(Formula f, byte origin) Transforms the goal into an implication formula
java.lang.Object	clone() Clones the goal
void	garbageIdent() Annotates all the fields that appear in the lemma to declare them in the Atelier B files.
void	getFields(java.util.Set fields)
Formula	getFormula() Returns the goal
java.util.Vector	getSubs() Returns the set of substitutions.
boolean	isOriginal() Returns the isOriginal.
void	oldParam(java.util.Vector e) Adds a old param around the element of the enumeration corresponding to the parameter of the method.
boolean	proveObvious(java.util.Vector hyp, boolean atTheEnd) A goal is obvious if the formula is obvious, if the formula appears in the hypothesis or if the goal comes from an invariant and it has not been modified during the complete generation.
void	setObvious(boolean b)
void	sub(Substitution s) Apply a substitution to the lemma.
void	suppressSpecialOld(int token) Suppress the Called Old expressions.

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

Goal

public Goal(VirtualFormula vf,
            GoalOrigin origin)

Constructs a goal from a formula and an origin.

Parameters:

vf - The formula corresponding to this goal.

origin - The origin of this goal

Goal

public Goal(Formula f,
            GoalOrigin origin)

Constructs a goal from a formula and an origin.

Parameters:

f - The formula corresponding to this goal.

origin - The origin of this goal

Method Detail

clone

public java.lang.Object clone()

Clones the goal

Returns:

the cloned goal

addImplicToGoal

public final void addImplicToGoal(Formula f,
                                  byte origin)

Transforms the goal into an implication formula

Parameters:

f - The implication antecedent

origin - The origin of f

oldParam

public final void oldParam(java.util.Vector e)

Description copied from interface: ILemma

Adds a old param around the element of the enumeration corresponding to the parameter of the method.

Specified by:

oldParam in interface ILemma

Parameters:

e - fields enumeration

See Also:

Theorem#oldParam(Enumeration)

sub

public final void sub(Substitution s)

Description copied from interface: ILemma

Apply a substitution to the lemma.

Specified by:

sub in interface ILemma

Parameters:

s - substitution to apply.

See Also:

Proofs.sub(Substitution)

suppressSpecialOld

public final void suppressSpecialOld(int token)

Description copied from interface: ILemma

Suppress the Called Old expressions.

Specified by:

suppressSpecialOld in interface ILemma

See Also:

Theorem#suppressCalledOld()

garbageIdent

public final void garbageIdent()

Description copied from interface: ILemma

Annotates all the fields that appear in the lemma to declare them in the Atelier B files.

Specified by:

garbageIdent in interface ILemma

See Also:

Theorem#garbageIdent()

proveObvious

public final boolean proveObvious(java.util.Vector hyp,
                                  boolean atTheEnd)

A goal is obvious if the formula is obvious, if the formula appears in the hypothesis or if the goal comes from an invariant and it has not been modified during the complete generation.

Specified by:

proveObvious in interface ILemma

Returns:

true if the goal is obvious, false otherwise

See Also:

Proofs.proveObvious(boolean, boolean)

getFields

public void getFields(java.util.Set fields)

getFormula

public Formula getFormula()

Returns the goal

Returns:

the formula corresponding to the goal

getSubs

public final java.util.Vector getSubs()

Returns the set of substitutions.

Returns:

subs

isOriginal

public boolean isOriginal()

Returns the isOriginal.

Returns:

boolean

setObvious

public void setObvious(boolean b)