jml2b.pog.lemma
Class Lemma

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

All Implemented Interfaces:

IFormToken, ILemma

Direct Known Subclasses:

jml2b.pog.lemma.BehaviourLemma, ExsuresLemma, SimpleLemma

public abstract class Lemma

extends Profiler

implements ILemma, IFormToken

This class defines a lemma. A lemma is the goal part of a theorem. A lemma can be:

• a simple lemma consisting in a list of goal
• a exsures lemma consisting in an exception and a simple lemma
• a normal behaviour lemma consisting in a set of labelled simple normal behaviours (requires, modifies, ensures)
• a exceptional behaviour lemma consisting in a set of labelled simple exceptional behaviours (requires, modifies, exsures).

Author:

L. Burdy

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

Lemma()

Method Summary

boolean	catches(AClass c) Returns whether a exsures lemma catches a given exception.
Lemma	catchException(Type type, Field catchParam) Returns the lemma corresponding to the current lemma encapsulated in the fact that it corresponds to a catch of an exception.
abstract java.lang.Object	clone() Clones a lemma.
abstract void	getFields(java.util.Set fields)
void	getTypesException(java.util.Set s) Collects all the exception type that are declared in the exsures lemma of this lemma.
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.
abstract void	selectLabel(java.util.Vector labels) Selects in the labelled lemmas, the cases corresponding to labels.
Lemma	throwException(Formula vv, Formula c) Returns the lemma to prove to ensure that the thrown of an exception ensures the current lemma.
Lemma	throwException(java.lang.String vv, AClass c) Returns the lemma to prove to ensure that the thrown of an exception ensures the current lemma.

Methods inherited from class jml2b.util.Profiler

runGC

Methods inherited from class java.lang.Object

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

Methods inherited from interface jml2b.pog.lemma.ILemma

garbageIdent, oldParam, proveObvious, sub, suppressSpecialOld

Constructor Detail

Lemma

public Lemma()

Method Detail

nbPo

public int nbPo()

Returns the number of goals.

Returns:

the number of goals in the lemma

Throws:

InternalError - when the method is called with a BehaviourLemma or a ExsuresLemma.

See Also:

Proofs.nbPo()

nbPoChecked

public int nbPoChecked()

nbPoProved

public int nbPoProved(java.lang.String prover)

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

Returns:

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

Throws:

InternalError - when the method is called with a BehaviourLemma or a ExsuresLemma.

See Also:

Proofs#nbProved(int)

nbPoProved

public int nbPoProved()

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

Returns:

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

Throws:

InternalError - when the method is called with a BehaviourLemma or a ExsuresLemma.

See Also:

Proofs#nbProved(int)

getTypesException

public void getTypesException(java.util.Set s)

Collects all the exception type that are declared in the exsures lemma of this lemma.

Parameters:

s - set of Type

Throws:

InternalError - when the method is called with a NormalLemma or a SimpleLemma.

See Also:

Theorem#getTypesException(Set)

getFields

public abstract void getFields(java.util.Set fields)

throwException

public Lemma throwException(Formula vv,
                            Formula c)

Returns the lemma to prove to ensure that the thrown of an exception ensures the current lemma.

Parameters:

vv - Instance of the thrown exception.

c - Formula containing the class of the thrown exception.

Returns:

the exsures lemmas corresponfing to the thrown exceptions

Throws:

InternalError - when the method is called with a NormalLemma or a SimpleLemma.

throwException

public Lemma throwException(java.lang.String vv,
                            AClass c)

Returns the lemma to prove to ensure that the thrown of an exception ensures the current lemma.

Parameters:

vv - Instance of the thrown exception.

c - Class of the thrown exception.

Returns:

the exsures lemmas corresponding to the thrown exceptions

Throws:

InternalError - when the method is called with a NormalLemma or a SimpleLemma.

catchException

public Lemma catchException(Type type,
                            Field catchParam)

Returns the lemma corresponding to the current lemma encapsulated in the fact that it corresponds to a catch of an exception.

Parameters:

type - catched exception

catchParam - catched parameter

Returns:

a lemma with exsures clause

Throws:

InternalError - when the method is called with a ExsuresLemma or a ExceptionalLemma.

clone

public abstract java.lang.Object clone()

Clones a lemma.

Returns:

the cloned lemma

selectLabel

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

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

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.

catches

public boolean catches(AClass c)

Returns whether a exsures lemma catches a given exception.

Parameters:

c - The class of the tested exception

Returns:

true if the exsures lemma of the current lemma contains an exception type that is a super type of the given class, false otherwise