jml2b.pog.lemma
Class SimpleLemma

java.lang.Object
  jml2b.util.Profiler
      jml2b.pog.lemma.Lemma
          jml2b.pog.lemma.SimpleLemma

All Implemented Interfaces:

IFormToken, ILemma, java.io.Serializable

Direct Known Subclasses:

VariantLemma

public class SimpleLemma

extends Lemma

implements java.io.Serializable

This class implements a simple lemma, that is a set of goals

Author:

L. Burdy

See Also:

Serialized Form

Field Summary

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

SimpleLemma()
Constructs a lemma with an empty set of goals

SimpleLemma(Formula f, GoalOrigin origin)
Constructs a lemma from a formula.

SimpleLemma(IJml2bConfiguration config, Expression f, GoalOrigin origin)
Constructs a lemma from an expression.

SimpleLemma(IJml2bConfiguration config, java.util.Vector v, GoalOrigin origin)
Constructs a lemma from a set of expression.

SimpleLemma(Lemma l)
Constructs a simple lemma containing only non obvious goals from a lemma.

SimpleLemma(java.util.Vector goals)
Constructs a lemma from a loaded one.

Method Summary

void	addGoal(Goal g) Adds a goal to the goal set
void	addGoals(SimpleLemma l) Concats two simple lemmas
void	addImplicToGoal(Formula f, byte origin) Transforms each goal into an implication formula
Lemma	catchException(Type type, Field catchParam) Returns an exsures lemma
java.lang.Object	clone() Clones the simple lemma
static java.util.Vector	coloredInfos(java.util.Vector pis, byte comment) Returns the set of ColoredInfo construct from a set of ParsedItem
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()
Goal	getGoal(int i) Returns a goal
java.util.Enumeration	getGoals() Returns the set of goals
void	mergeWith(Goal[] goals) Merges the lemma with a loaded set of lemmas.
int	nbPo() Returns the number of goals.
int	nbPoChecked()
int	nbPoProved() Returns the number of goals that are in a specified state.
int	nbPoProved(java.lang.String prover) Returns the number of goals that are in a specified state.
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) Supress in the lemma the obvious goals.
void	save(IJml2bConfiguration config, JpoOutputStream s, JmlFile jf)
void	selectLabel(java.util.Vector labels) Selects in the labelled lemmas, the cases corresponding to labels.
void	sub(Substitution s) Apply a substitution to the lemma.
void	suppressSpecialOld(int token) Suppress the Called Old expressions.

Methods inherited from class jml2b.pog.lemma.Lemma

catches, getTypesException, throwException, throwException

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

SimpleLemma

public SimpleLemma()

Constructs a lemma with an empty set of goals

SimpleLemma

public SimpleLemma(IJml2bConfiguration config,
                   Expression f,
                   GoalOrigin origin)
            throws Jml2bException,
                   PogException

Constructs a lemma from an expression. If the expression is conjonctive, each part of the conjonction becomes a goal

Parameters:

config - The current configuration

f - The expression

origin - The origin to assign to created goals

SimpleLemma

public SimpleLemma(Formula f,
                   GoalOrigin origin)

Constructs a lemma from a formula.

Parameters:

f - The formula

origin - The origin to assign to created goals

SimpleLemma

public SimpleLemma(IJml2bConfiguration config,
                   java.util.Vector v,
                   GoalOrigin origin)
            throws Jml2bException,
                   PogException

Constructs a lemma from a set of expression. If the expression is conjonctive, each part of the conjonction becomes a goal

Parameters:

config - The current configuration

v - The set of expression

origin - The origin to assign to created goals

SimpleLemma

public SimpleLemma(java.util.Vector goals)

Constructs a lemma from a loaded one.

Parameters:

goals - The set of loaded goals

SimpleLemma

public SimpleLemma(Lemma l)

Constructs a simple lemma containing only non obvious goals from a lemma. This is performed at the end of the wp calculus to convert all lemma into simple lemma

Parameters:

l - The lemma to convert

Method Detail

coloredInfos

public static java.util.Vector coloredInfos(java.util.Vector pis,
                                            byte comment)

Returns the set of ColoredInfo construct from a set of ParsedItem

Parameters:

pis - The set of ParsedItem

Returns:

a vector containing each parsed item converted in a colored info

clone

public java.lang.Object clone()

Clones the simple lemma

Specified by:

clone in class Lemma

Returns:

the cloned simple lemma

addGoals

public void addGoals(SimpleLemma l)

Concats two simple lemmas

Parameters:

l - The simple lemma to concat

addGoal

public void addGoal(Goal g)

Adds a goal to the goal set

Parameters:

g - The goal to add

addImplicToGoal

public void addImplicToGoal(Formula f,
                            byte origin)

Transforms each goal into an implication formula

Parameters:

f - The implication antecedent

origin - The origin of f

nbPo

public int nbPo()

Description copied from class: Lemma

Returns the number of goals.

Overrides:

nbPo in class Lemma

Returns:

the size of the goals set

See Also:

Proofs.nbPo()

nbPoProved

public int nbPoProved(java.lang.String prover)

Description copied from class: Lemma

Returns the number of goals that are in a specified state.

Overrides:

nbPoProved in class Lemma

Returns:

the number of goals in the lemma which have a state equals to the paremeter.

See Also:

Proofs#nbProved(int)

nbPoProved

public int nbPoProved()

Description copied from class: Lemma

Returns the number of goals that are in a specified state.

Overrides:

nbPoProved in class Lemma

Returns:

the number of goals in the lemma which have a state equals to the paremeter.

See Also:

Proofs#nbProved(int)

nbPoChecked

public int nbPoChecked()

Overrides:

nbPoChecked in class Lemma

oldParam

public 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 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 void suppressSpecialOld(int token)

Description copied from interface: ILemma

Suppress the Called Old expressions.

Specified by:

suppressSpecialOld in interface ILemma

See Also:

Theorem#suppressCalledOld()

save

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

Throws:

java.io.IOException

proveObvious

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

Description copied from interface: ILemma

Supress in the lemma the obvious goals.

Specified by:

proveObvious in interface ILemma

Returns:

true if the lemma contains only obvious goals, false otherwise.

See Also:

Proofs.proveObvious(boolean, boolean)

garbageIdent

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

getFields

public void getFields(java.util.Set fields)

Specified by:

getFields in class Lemma

catchException

public Lemma catchException(Type type,
                            Field catchParam)

Returns an exsures lemma

Overrides:

catchException in class Lemma

Parameters:

type - catched exception

catchParam - catched parameter

Returns:

a lemma with exsures clause

selectLabel

public void selectLabel(java.util.Vector labels)
                 throws WrongLabelException

Description copied from class: Lemma

Selects in the labelled lemmas, the cases corresponding to labels.

Specified by:

selectLabel in class Lemma

Parameters:

labels - set of labels that have to be selected

Throws:

WrongLabelException - if a behaviour lemma does not contain any remaining case after the selection.

mergeWith

public void mergeWith(Goal[] goals)

Merges the lemma with a loaded set of lemmas.

getFormula

public Formula getFormula()

Returns:

the formula corresponding to the conjonction of all the goals

getGoals

public java.util.Enumeration getGoals()

Returns the set of goals

getGoal

public Goal getGoal(int i)

Returns a goal

Parameters:

i - The goal index

Returns:

The goal at index i