jml2b.pog.lemma
Class ExsuresLemma

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

All Implemented Interfaces:

IFormToken, ILemma

public class ExsuresLemma

extends Lemma

This class contains the information extracted from an exsures pragma.

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

ExsuresLemma(IJml2bConfiguration config, Exsures ex, Expression b, GoalOrigin origin)
Constructs an exsures lemma from an exsures clause

ExsuresLemma(IJml2bConfiguration config, Exsures ex, GoalOrigin origin)
Constructs an exsures lemma from an exsures clause

ExsuresLemma(Type t, Field f, SimpleLemma p)
Constructs an exsures lemma

Method Summary

boolean	catches(AClass c) Returns whether a exsures lemma catches a given exception.
java.lang.Object	clone() Clones a lemma.
void	garbageIdent() Annotates all the fields that appear in the lemma to declare them in the Atelier B files.
java.lang.String	getBName() Returns the name of the catched variable or a temporary variable if there is no catched variable
Field	getExceptionField()
Type	getExceptionType() Returns the exceptionType.
void	getFields(java.util.Set fields)
SimpleLemma	getLemma() Returns the lemma.
void	getTypesException(java.util.Set s) Adds the exception type to the set
Proofs	impliesExceptional(ExceptionalBehaviourStack ebs) Returns the proof that the exsures lemma implies an exceptionnal behaviour.
void	oldParam(java.util.Vector enum) 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	selectLabel(java.util.Vector labels) Selects in the labelled lemmas, the cases corresponding to labels.
void	setExceptionType(Type exceptionType) Sets the exceptionType.
void	sub(Substitution s) Apply a substitution to the lemma.
void	suppressSpecialOld(int token) Suppress the Called Old expressions.
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.pog.lemma.Lemma

catchException, nbPo, nbPoChecked, nbPoProved, nbPoProved

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

ExsuresLemma

public ExsuresLemma(Type t,
                    Field f,
                    SimpleLemma p)

Constructs an exsures lemma

Parameters:

t - The exception type

f - The catched variable

p - The associated lemma

ExsuresLemma

public ExsuresLemma(IJml2bConfiguration config,
                    Exsures ex,
                    Expression b,
                    GoalOrigin origin)
             throws Jml2bException,
                    PogException

Constructs an exsures lemma from an exsures clause

Parameters:

config - The current configuration

ex - The exsures clause

b - The expression that should be used to instancie the clause

origin - The origin of the exsures clause, it can come from a method or a loop

Throws:

PogException

Jml2bException

ExsuresLemma

public ExsuresLemma(IJml2bConfiguration config,
                    Exsures ex,
                    GoalOrigin origin)
             throws Jml2bException,
                    PogException

Constructs an exsures lemma from an exsures clause

Parameters:

config - The current configuration

ex - The exsures clause

origin - The origin of the exsures clause, it can come from a method or a loop

Throws:

PogException

Jml2bException

Method Detail

clone

public java.lang.Object clone()

Description copied from class: Lemma

Clones a lemma.

Specified by:

clone in class Lemma

Returns:

the cloned lemma

getBName

public java.lang.String getBName()

Returns the name of the catched variable or a temporary variable if there is no catched variable

Returns:

a name for the catched variable

throwException

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

Description copied from class: Lemma

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

Overrides:

throwException in class Lemma

Parameters:

vv - Instance of the thrown exception.

c - Class of the thrown exception.

Returns:

the lemma where the exception field has been substituted with vv if c is a subtype of the exception type.

throwException

public Lemma throwException(Formula vv,
                            Formula c)

Description copied from class: Lemma

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

Overrides:

throwException in class Lemma

Parameters:

vv - Instance of the thrown exception.

c - Formula containing the class of the thrown exception.

Returns:

the lemma under the implication that c is a subtype of the excpetion type where the exception field has been substituted with vv.

oldParam

public void oldParam(java.util.Vector enum)

Description copied from interface: ILemma

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

Parameters:

enum - fields enumeration

See Also:

Theorem#oldParam(Enumeration)

suppressSpecialOld

public void suppressSpecialOld(int token)

Description copied from interface: ILemma

Suppress the Called Old expressions.

See Also:

Theorem#suppressCalledOld()

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.

See Also:

Theorem#garbageIdent()

sub

public void sub(Substitution s)

Description copied from interface: ILemma

Apply a substitution to the lemma.

Parameters:

s - substitution to apply.

See Also:

Proofs.sub(Substitution)

proveObvious

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

Description copied from interface: ILemma

Supress in the lemma the obvious goals.

Returns:

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

See Also:

Proofs.proveObvious(boolean, boolean)

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.

getTypesException

public void getTypesException(java.util.Set s)

Adds the exception type to the set

Overrides:

getTypesException in class Lemma

Parameters:

s - set of Type

See Also:

Theorem#getTypesException(Set)

getFields

public void getFields(java.util.Set fields)

Specified by:

getFields in class Lemma

impliesExceptional

public Proofs impliesExceptional(ExceptionalBehaviourStack ebs)

Returns the proof that the exsures lemma implies an exceptionnal behaviour.

Parameters:

ebs - The exceptional behaviour

Returns:

the calculated proof

catches

public boolean catches(AClass c)

Description copied from class: Lemma

Returns whether a exsures lemma catches a given exception.

Overrides:

catches in class Lemma

Parameters:

c - The class of the tested exception

Returns:

whether c is a subclass of the exception type.

getExceptionType

public Type getExceptionType()

Returns the exceptionType.

Returns:

exceptionType

getLemma

public SimpleLemma getLemma()

Returns the lemma.

Returns:

lemma

setExceptionType

public void setExceptionType(Type exceptionType)

Sets the exceptionType.

Parameters:

exceptionType - The exceptionType to set

getExceptionField

public Field getExceptionField()

Returns: