jml2b.pog.util
Class ContextFromPureMethod

java.lang.Object
  jml2b.util.Profiler
      jml2b.pog.util.ContextFromPureMethod

All Implemented Interfaces:

IFormToken

public class ContextFromPureMethod

extends Profiler

implements IFormToken

This class contains the context issued from pure method that is used when translating an expression into a formula. When the expression to translate does not contain any call to a pure method, only the field f is usefull and contains the result of the translation. When the expression contains calls to pure method, a context is returned containing the returned variable choosen for theis method and its ensures clause. For example the expression m() == 3 with m ensures : \result <= 2 will be translated in \forall byte r; r <= 2 ==> r == 3 and temporary during the translation m() is translated in a context where results contains the field r of type byte, ensures contains r <= 2 and f contains r. The context is translated into a formula with it is possible, i.e. when the expression becomes a predicate. For example, when translating m() + m() == 3, the two contexts will be concatened before being translated (when the equality will be translated).

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

ContextFromPureMethod(ContextFromPureMethod c1, ContextFromPureMethod c2, ContextFromPureMethod c3, Formula f)
Constructs a context from the translation of a 3-ary operator.

ContextFromPureMethod(ContextFromPureMethod c1, ContextFromPureMethod c2, Formula f)
Constructs a context from the translation of a binary operator.

ContextFromPureMethod(ContextFromPureMethod c, Formula f)
Constructs a context from an existing context and a formula.

ContextFromPureMethod(ContextFromPureMethod c, java.lang.String res, Formula f, Type t, Formula ens)
Constructs a context from a method call with parameter.

ContextFromPureMethod(Formula f)
Constructs a context form a formula, the context is empty.

ContextFromPureMethod(java.lang.String f, Formula res, Type t, Formula ens)
Constructs a context from a method call without parameter.

Method Summary

Formula	getFormula() Returns the formula.
Formula	getFormulaWithContext() Returns the result of the translation.

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

ContextFromPureMethod

public ContextFromPureMethod(Formula f)

Constructs a context form a formula, the context is empty.

Parameters:

f - formula resulting form the translation of an expression without method call or from a expression that is a predicate.

ContextFromPureMethod

public ContextFromPureMethod(ContextFromPureMethod c,
                             Formula f)

Constructs a context from an existing context and a formula.

Parameters:

c - context that is taken into account, except its formula.

f - formula resulting form the translation of an expression without method call or from a expression that is a predicate.

ContextFromPureMethod

public ContextFromPureMethod(java.lang.String f,
                             Formula res,
                             Type t,
                             Formula ens)

Constructs a context from a method call without parameter.

Parameters:

res - the field corresponding to the result of the call

t - the returned type of the method called

ens - the ensures clause of the method called

ContextFromPureMethod

public ContextFromPureMethod(ContextFromPureMethod c,
                             java.lang.String res,
                             Formula f,
                             Type t,
                             Formula ens)

Constructs a context from a method call with parameter.

Parameters:

c - context issued from the translation of the parameters.

res - the field corresponding to the result of the call

t - the returned type of the method called

ens - the ensures clause of the method called

ContextFromPureMethod

public ContextFromPureMethod(ContextFromPureMethod c1,
                             ContextFromPureMethod c2,
                             Formula f)

Constructs a context from the translation of a binary operator.

Parameters:

c1 - context issued form the translation of one part.

c2 - context issued form the translation of the other part.

f - translation resulting formula

ContextFromPureMethod

public ContextFromPureMethod(ContextFromPureMethod c1,
                             ContextFromPureMethod c2,
                             ContextFromPureMethod c3,
                             Formula f)

Constructs a context from the translation of a 3-ary operator.

Parameters:

c1 - context issued form the translation of a part.

c2 - context issued form the translation of another part.

c3 - context issued form the translation of another part.

f - translation resulting formula

Method Detail

getFormulaWithContext

public Formula getFormulaWithContext()

Returns the result of the translation.

Returns:

the formula quantified by the contextual part.

getFormula

public Formula getFormula()

Returns the formula.

Returns:

the formula without its context.