jml2b.pog.lemma
Class ExceptionalBehaviourStack

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

All Implemented Interfaces:

IFormToken

public class ExceptionalBehaviourStack

extends Profiler

implements IFormToken

This class describes a stack of proof obligations associated to exceptional behaviours.

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

ExceptionalBehaviourStack(ExceptionalProofs eb)
Constructs a stack with one element.

Method Summary

ExceptionalBehaviourStack	addAll(ExceptionalBehaviourStack ebs) Concats two stacks.
java.lang.Object	clone() Clones the stack
ExceptionalBehaviourStack	finallyOnExceptionalBehaviour(IJml2bConfiguration config, Statement body, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour) Calculate the ExceptionalProofs stack resulting from the application of the body on the current stack (used to proceed a finally).
static ExceptionalBehaviourStack	getFalse(IJml2bConfiguration config)
ExceptionalBehaviourStack	pop(int i) Pop elements from the stack
ExceptionalBehaviourStack	push(ExceptionalProofs eb) Push an element on top of the stack
int	size() Returns the size of the stack
Proofs	throwException(Formula vv, Formula c) Returns the proof to prove to ensure that the thrown of an exception ensures the current proof.
Proofs	throwException(IJml2bConfiguration config, AClass c) Calculates the proof obligation ensuring that the thrown of a runtime exception ensures the current proof.
Proofs	throwException(java.lang.String vv, AClass c) Returns the proof obligation ensuring that the thrown of an exception ensures the current proof.

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

ExceptionalBehaviourStack

public ExceptionalBehaviourStack(ExceptionalProofs eb)

Constructs a stack with one element.

Parameters:

eb - The element on top of the stack

Method Detail

getFalse

public static ExceptionalBehaviourStack getFalse(IJml2bConfiguration config)
                                          throws Jml2bException,
                                                 PogException

Throws:

Jml2bException

PogException

clone

public java.lang.Object clone()

Clones the stack

Returns:

the cloned stack

size

public int size()

Returns the size of the stack

Returns:

the number of element of the stack

push

public ExceptionalBehaviourStack push(ExceptionalProofs eb)

Push an element on top of the stack

Parameters:

eb - The proof to push

Returns:

the new stack

pop

public ExceptionalBehaviourStack pop(int i)

Pop elements from the stack

Parameters:

i - The number of elements to pop

Returns:

the new stack

addAll

public ExceptionalBehaviourStack addAll(ExceptionalBehaviourStack ebs)

Concats two stacks.

Parameters:

ebs - The stack to concat to the current one

Returns:

a stack consisting on the two stacks concatened

throwException

public Proofs throwException(Formula vv,
                             Formula c)

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

Parameters:

vv - Instance of the thrown exception.

c - Formula containing the class of the thrown exception.

throwException

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

Returns the proof obligation ensuring that the thrown of an exception ensures the current proof.

Parameters:

vv - The instance of the thrown exception.

c - The class of the thrown exception.

throwException

public Proofs throwException(IJml2bConfiguration config,
                             AClass c)
                      throws Jml2bException,
                             PogException

Calculates the proof obligation ensuring that the thrown of a runtime exception ensures the current proof.

Parameters:

config - The current configuration

c - The class of the thrown exception.

Throws:

PogException

Jml2bException

finallyOnExceptionalBehaviour

public ExceptionalBehaviourStack finallyOnExceptionalBehaviour(IJml2bConfiguration config,
                                                               Statement body,
                                                               Proofs finishOnReturn,
                                                               LabeledProofsVector finishOnBreakLab,
                                                               LabeledProofsVector finishOnContinueLab,
                                                               ExceptionalBehaviourStack exceptionalBehaviour)
                                                        throws Jml2bException,
                                                               PogException

Calculate the ExceptionalProofs stack resulting from the application of the body on the current stack (used to proceed a finally).

Parameters:

config - The current configuration

body - The finally body

finishOnReturn - theorems to ensure if the statement terminates abruptly on a return

finishOnBreakLab - labelled theorems to ensure if the statement terminates abruptly on a break

finishOnContinueLab - labelled theorems to ensure if the statement terminates abruptly on a continue

exceptionalBehaviour - exceptional theorems to ensure if the statement terminates abruply on an exception

Returns:

the new stack

Throws:

PogException

Jml2bException