jml2b.pog.lemma
Class ExceptionalLemma

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

All Implemented Interfaces:

IFormToken, ILemma

public class ExceptionalLemma

extends jml2b.pog.lemma.BehaviourLemma

This class defines lemmas resulting from the proof of an exceptional method specification. ensuresLemmas is a set of ExsuresLabelledLemma

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

ExceptionalLemma(IJml2bConfiguration config, Method m, java.util.Vector fields, SimpleLemma l, SimpleLemma sco, SimpleLemma ico)
Creates a set of exsures labelled lemma corresponding to the cases of a method specification corresponding to exceptional behaviours.

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.
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.
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	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

ExceptionalLemma

public ExceptionalLemma(IJml2bConfiguration config,
                        Method m,
                        java.util.Vector fields,
                        SimpleLemma l,
                        SimpleLemma sco,
                        SimpleLemma ico)
                 throws Jml2bException,
                        PogException

Creates a set of exsures labelled lemma corresponding to the cases of a method specification corresponding to exceptional behaviours.

Parameters:

config - The current configuration

m - The analyzed method

fields - The set of modifiable fields

l - The current invariant

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

getTypesException

public void getTypesException(java.util.Set s)

Description copied from class: Lemma

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

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

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 exsures lemmas corresponfing to the thrown exceptions

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 exsures lemmas corresponding to the thrown exceptions

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:

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

proveObvious

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

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.

See Also:

Theorem#garbageIdent()

oldParam

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

sub

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

suppressSpecialOld

public final void suppressSpecialOld(int token)

Description copied from interface: ILemma

Suppress the Called Old expressions.

See Also:

Theorem#suppressCalledOld()

selectLabel

public final 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.