jml2b.formula
Interface IFormToken

All Known Subinterfaces:

Substitution

All Known Implementing Classes:

ContextFromPureMethod, ExceptionalBehaviourStack, Expression, Formula, Goal, Lemma, Modifies, ModifiesClause, Pog, Proofs, SourceProofObligation, SpecArray, Statement, StLabel, SubArrayElement, SubArrayElementSingle, SubArrayLength, SubForm, SubInstances, SubInstancesSet, SubMemberField, SubTmpVar, SubTypeof, Theorem

public interface IFormToken

This interface defines the token associated to formulas corresponding to operators. Those token come from Java token (Ja_xxx), Jml token (Jm_xxx) or B token (B_xxx). A priority is associated to each operator.

Author:

L. Burdy

Field Summary

static byte	ARRAY_ACCESS
static byte	ARRAY_RANGE array range UNION(x).(x : a | b[c]) with priority 250.
static byte	B_ACCOLADE B bracket unary operator {a} with priority 250.
static byte	B_APPLICATION B application binary operator a(b) with priority 250
static byte	B_ARRAY_EQUALS B function equality operator with priority 50.
static byte	B_BOOL B boolean unary operator bool(a) with priority 250
static byte	B_BTRUE B literal btrue 0=0 with priority 250.
static byte	B_COUPLE B couple binary operator a |-> b with priority 250.
static byte	B_DOM B domaine function with priority 250
static byte	B_FUNCTION_EQUALS B function equality operator with priority 50.
static byte	B_IN B belongs to binary operator a : b with priority 60
static byte	B_INTERVAL B interval binary operator a ..
static byte	B_OVERRIDING B overriding binary operator a <+ b with priority 90.
static byte	B_SET_EQUALS B set equality operator with priority 50.
static byte	B_SUBSTRACTION_DOM B substraction dom operator with priority 40.
static byte	B_UNION B union binary operator a \/ b with priority 140.
static byte	CONSTANT_FUNCTION constant function a * {b} with priority 200.
static byte	CONSTANT_FUNCTION_FUNCTION constant function function a * {b * {c}} with priority 200.
static byte	EQUALS_ON_OLD_INSTANCES Domain restriction equality operator a <| b == a <| c with priority 50.
static byte	EQUALS_ON_OLD_INSTANCES_ARRAY Domain restriction equality operator a <| b == a <| c with priority 50.
static byte	FINAL_IDENT Constant identifier with priority 250.
static byte	GUARDED_SET Set guarded by a condition
static byte	INTERSECTION_IS_NOT_EMPTY B intersection binary operator a /\ b /= {} with priority 160.
static byte	IS_ARRAY B total injection binary operator a >-> b with priority 120.
static byte	IS_MEMBER_FIELD B partial function binary operator a +-> b with priority 120.
static byte	IS_STATIC_FIELD
static byte	Ja_ADD_OP Additive binary operator a + b with priority 180.
static byte	Ja_AND_OP Conjonction binary operator a && b with priority 40.
static byte	Ja_CHAR_LITERAL Character literal with priority 250.
static byte	Ja_COMMA Comma binary operator a , b with priority 70.
static byte	Ja_DIFFERENT_OP Different binary operator a != b with priority 50.
static byte	Ja_DIV_OP Division binary operator a / b with priority 190.
static byte	Ja_EQUALS_OP Equality binary operator a == b with priority 50.
static byte	Ja_GE_OP Greater or equal binary operator a >= b with priority 50.
static byte	Ja_GREATER_OP Strictly greater binary operator a > b with priority 50.
static byte	Ja_IDENT Identifier a with priority 250.
static byte	Ja_JAVA_BUILTIN_TYPE Java builtin type with priority 250.
static byte	Ja_LE_OP Less or equal binary operator a <= b with priority 50.
static byte	Ja_LESS_OP Strictly less binary operator a < b with priority 50.
static byte	Ja_LITERAL_false Literal false with priority 250.
static byte	Ja_LITERAL_null Literal null with priority 250.
static byte	Ja_LITERAL_super Literal super with priority 250.
static byte	Ja_LITERAL_this Literal this with priority 250.
static byte	Ja_LITERAL_true Literal true with priority 250.
static byte	Ja_LNOT Negation unary operator !a with priority 250.
static byte	Ja_MOD Modulo binary operator a mod b with priority 190.
static byte	Ja_MUL_OP Multiplicative binary operator a * b with priority 190.
static byte	Ja_NEGATIVE_OP Minus binary operator a - b with priority 180.
static byte	Ja_NUM_INT Integer literal with priority 250.
static byte	Ja_OR_OP Disjonctive binary operator a || b with priority 40.
static byte	Ja_QUESTION Question tri-ary operator a ? b : c with priority 90.
static byte	Ja_STRING_LITERAL String literal "aaa" with priority 250.
static byte	Ja_UNARY_NUMERIC_OP Unary minus operator -a with priority 210.
static byte	Jm_AND_THEN
static byte	Jm_EXISTS B existential quantifier operator #a.b with priority 250.
static byte	Jm_FORALL B universal quantification operator !a.b with priority 250.
static byte	Jm_IMPLICATION_OP JML Implication binary operator a ==> b with priority 30.
static byte	Jm_IS_SUBTYPE JML subtype binary operator a <: b with priority 250.
static byte	Jm_OR_ELSE
static byte	Jm_T_OLD JML old unary operator \old(a) with priority 250.
static byte	Jm_T_RESULT JML literal \result with priority 250.
static byte	Jm_T_TYPE JML type unary operator \type(a) with priority 250.
static byte	LOCAL_ELEMENTS_DECL Local xxxelements declaration corresponding formally to a B_IN
static byte	LOCAL_VAR_DECL Local variable declaration corresponding formally to a B_IN
static byte	MODIFIED_FIELD identifier corresponding to a modified field.
static byte	NEW_OBJECT
static byte	T_CALLED_OLD Called old operator with priority 250.
static byte	T_TYPE
static byte	T_VARIANT_OLD
static java.lang.String[]	toString Array given token name for the error displaying.

Field Detail

Ja_ADD_OP

public static final byte Ja_ADD_OP

Additive binary operator a + b with priority 180.

See Also:

Constant Field Values

Ja_EQUALS_OP

public static final byte Ja_EQUALS_OP

Equality binary operator a == b with priority 50.

See Also:

Constant Field Values

Ja_AND_OP

public static final byte Ja_AND_OP

Conjonction binary operator a && b with priority 40.

See Also:

Constant Field Values

Ja_MUL_OP

public static final byte Ja_MUL_OP

Multiplicative binary operator a * b with priority 190.

See Also:

Constant Field Values

Ja_LE_OP

public static final byte Ja_LE_OP

Less or equal binary operator a <= b with priority 50.

See Also:

Constant Field Values

Ja_UNARY_NUMERIC_OP

public static final byte Ja_UNARY_NUMERIC_OP

Unary minus operator -a with priority 210.

See Also:

Constant Field Values

Ja_IDENT

public static final byte Ja_IDENT

Identifier a with priority 250.

See Also:

Constant Field Values

Ja_COMMA

public static final byte Ja_COMMA

Comma binary operator a , b with priority 70.

See Also:

Constant Field Values

Ja_LITERAL_this

public static final byte Ja_LITERAL_this

Literal this with priority 250.

See Also:

Constant Field Values

Ja_MOD

public static final byte Ja_MOD

Modulo binary operator a mod b with priority 190.

See Also:

Constant Field Values

Ja_LNOT

public static final byte Ja_LNOT

Negation unary operator !a with priority 250.

See Also:

Constant Field Values

Ja_LITERAL_true

public static final byte Ja_LITERAL_true

Literal true with priority 250.

See Also:

Constant Field Values

Ja_LITERAL_false

public static final byte Ja_LITERAL_false

Literal false with priority 250.

See Also:

Constant Field Values

Ja_LITERAL_null

public static final byte Ja_LITERAL_null

Literal null with priority 250.

See Also:

Constant Field Values

Ja_NUM_INT

public static final byte Ja_NUM_INT

Integer literal with priority 250.

See Also:

Constant Field Values

Ja_CHAR_LITERAL

public static final byte Ja_CHAR_LITERAL

Character literal with priority 250.

See Also:

Constant Field Values

Ja_JAVA_BUILTIN_TYPE

public static final byte Ja_JAVA_BUILTIN_TYPE

Java builtin type with priority 250.

See Also:

Constant Field Values

Ja_LITERAL_super

public static final byte Ja_LITERAL_super

Literal super with priority 250.

See Also:

Constant Field Values

Ja_STRING_LITERAL

public static final byte Ja_STRING_LITERAL

String literal "aaa" with priority 250.

See Also:

Constant Field Values

Ja_NEGATIVE_OP

public static final byte Ja_NEGATIVE_OP

Minus binary operator a - b with priority 180.

See Also:

Constant Field Values

Ja_OR_OP

public static final byte Ja_OR_OP

Disjonctive binary operator a || b with priority 40.

See Also:

Constant Field Values

Ja_DIFFERENT_OP

public static final byte Ja_DIFFERENT_OP

Different binary operator a != b with priority 50.

See Also:

Constant Field Values

Ja_LESS_OP

public static final byte Ja_LESS_OP

Strictly less binary operator a < b with priority 50.

See Also:

Constant Field Values

Ja_GE_OP

public static final byte Ja_GE_OP

Greater or equal binary operator a >= b with priority 50.

See Also:

Constant Field Values

Ja_GREATER_OP

public static final byte Ja_GREATER_OP

Strictly greater binary operator a > b with priority 50.

See Also:

Constant Field Values

Ja_DIV_OP

public static final byte Ja_DIV_OP

Division binary operator a / b with priority 190.

See Also:

Constant Field Values

Ja_QUESTION

public static final byte Ja_QUESTION

Question tri-ary operator a ? b : c with priority 90.

See Also:

Constant Field Values

Jm_T_RESULT

public static final byte Jm_T_RESULT

JML literal \result with priority 250.

See Also:

Constant Field Values

Jm_IMPLICATION_OP

public static final byte Jm_IMPLICATION_OP

JML Implication binary operator a ==> b with priority 30.

See Also:

Constant Field Values

Jm_T_OLD

public static final byte Jm_T_OLD

JML old unary operator \old(a) with priority 250.

See Also:

Constant Field Values

Jm_T_TYPE

public static final byte Jm_T_TYPE

JML type unary operator \type(a) with priority 250.

See Also:

Constant Field Values

Jm_IS_SUBTYPE

public static final byte Jm_IS_SUBTYPE

JML subtype binary operator a <: b with priority 250.

See Also:

Constant Field Values

B_BTRUE

public static final byte B_BTRUE

B literal btrue 0=0 with priority 250.

See Also:

Constant Field Values

B_ACCOLADE

public static final byte B_ACCOLADE

B bracket unary operator {a} with priority 250.

See Also:

Constant Field Values

B_OVERRIDING

public static final byte B_OVERRIDING

B overriding binary operator a <+ b with priority 90.

See Also:

Constant Field Values

B_UNION

public static final byte B_UNION

B union binary operator a \/ b with priority 140.

See Also:

Constant Field Values

Jm_FORALL

public static final byte Jm_FORALL

B universal quantification operator !a.b with priority 250.

See Also:

Constant Field Values

CONSTANT_FUNCTION

public static final byte CONSTANT_FUNCTION

constant function a * {b} with priority 200.

See Also:

Constant Field Values

IS_ARRAY

public static final byte IS_ARRAY

B total injection binary operator a >-> b with priority 120.

See Also:

Constant Field Values

B_INTERVAL

public static final byte B_INTERVAL

B interval binary operator a .. b with priority 170.

See Also:

Constant Field Values

B_APPLICATION

public static final byte B_APPLICATION

B application binary operator a(b) with priority 250

See Also:

Constant Field Values

B_IN

public static final byte B_IN

B belongs to binary operator a : b with priority 60

See Also:

Constant Field Values

B_BOOL

public static final byte B_BOOL

B boolean unary operator bool(a) with priority 250

See Also:

Constant Field Values

B_COUPLE

public static final byte B_COUPLE

B couple binary operator a |-> b with priority 250.

See Also:

Constant Field Values

IS_MEMBER_FIELD

public static final byte IS_MEMBER_FIELD

B partial function binary operator a +-> b with priority 120.

See Also:

Constant Field Values

Jm_EXISTS

public static final byte Jm_EXISTS

B existential quantifier operator #a.b with priority 250.

See Also:

Constant Field Values

EQUALS_ON_OLD_INSTANCES

public static final byte EQUALS_ON_OLD_INSTANCES

Domain restriction equality operator a <| b == a <| c with priority 50.

See Also:

Constant Field Values

FINAL_IDENT

public static final byte FINAL_IDENT

Constant identifier with priority 250.

See Also:

Constant Field Values

T_CALLED_OLD

public static final byte T_CALLED_OLD

Called old operator with priority 250.

See Also:

Constant Field Values

LOCAL_VAR_DECL

public static final byte LOCAL_VAR_DECL

Local variable declaration corresponding formally to a B_IN

See Also:

Constant Field Values

GUARDED_SET

public static final byte GUARDED_SET

Set guarded by a condition

See Also:

Constant Field Values

INTERSECTION_IS_NOT_EMPTY

public static final byte INTERSECTION_IS_NOT_EMPTY

B intersection binary operator a /\ b /= {} with priority 160.

See Also:

Constant Field Values

ARRAY_RANGE

public static final byte ARRAY_RANGE

array range UNION(x).(x : a | b[c]) with priority 250.

See Also:

Constant Field Values

B_DOM

public static final byte B_DOM

B domaine function with priority 250

See Also:

Constant Field Values

B_SET_EQUALS

public static final byte B_SET_EQUALS

B set equality operator with priority 50.

See Also:

Constant Field Values

B_SUBSTRACTION_DOM

public static final byte B_SUBSTRACTION_DOM

B substraction dom operator with priority 40.

See Also:

Constant Field Values

B_FUNCTION_EQUALS

public static final byte B_FUNCTION_EQUALS

B function equality operator with priority 50.

See Also:

Constant Field Values

CONSTANT_FUNCTION_FUNCTION

public static final byte CONSTANT_FUNCTION_FUNCTION

constant function function a * {b * {c}} with priority 200.

See Also:

Constant Field Values

MODIFIED_FIELD

public static final byte MODIFIED_FIELD

identifier corresponding to a modified field.

See Also:

Constant Field Values

T_VARIANT_OLD

public static final byte T_VARIANT_OLD

See Also:

Constant Field Values

NEW_OBJECT

public static final byte NEW_OBJECT

See Also:

Constant Field Values

EQUALS_ON_OLD_INSTANCES_ARRAY

public static final byte EQUALS_ON_OLD_INSTANCES_ARRAY

Domain restriction equality operator a <| b == a <| c with priority 50.

See Also:

Constant Field Values

T_TYPE

public static final byte T_TYPE

See Also:

Constant Field Values

IS_STATIC_FIELD

public static final byte IS_STATIC_FIELD

See Also:

Constant Field Values

ARRAY_ACCESS

public static final byte ARRAY_ACCESS

See Also:

Constant Field Values

Jm_AND_THEN

public static final byte Jm_AND_THEN

See Also:

Constant Field Values

Jm_OR_ELSE

public static final byte Jm_OR_ELSE

See Also:

Constant Field Values

B_ARRAY_EQUALS

public static final byte B_ARRAY_EQUALS

B function equality operator with priority 50.

See Also:

Constant Field Values

LOCAL_ELEMENTS_DECL

public static final byte LOCAL_ELEMENTS_DECL

Local xxxelements declaration corresponding formally to a B_IN

See Also:

Constant Field Values

toString

public static final java.lang.String[] toString

Array given token name for the error displaying.