jml2b.languages.java
Class JavaBinaryForm

java.lang.Object
  jml2b.util.Profiler
      jml2b.formula.Formula
          jml2b.formula.BinaryForm
              jml2b.languages.java.JavaBinaryForm

All Implemented Interfaces:

IFormToken, ITranslatable, java.io.Serializable

public class JavaBinaryForm

extends BinaryForm

implements ITranslatable

Author:

L. Burdy

See Also:

Serialized Form

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

Method Summary

ITranslationResult

toLang(int indent) Converts the binary formula to a string suitable for output into the Java view.

Methods inherited from class jml2b.formula.BinaryForm

clone, contains, equals, garbageIdent, getBasicType, getDefaultRefDecl, getDefaultRefDecl, getFields, getLeft, getRight, instancie, is, isObvious, processIdent, renameParam, save, sub, subIdent, suppressSpecialOld, toVector

Methods inherited from class jml2b.formula.Formula

and, create, declarField, domainRestrict, getFalse, getNodeType, getNull, implies, indent, isBFalse, matchAEqualsNull, not, oldParam, or, renameParam, sub, toJava, toLang

Methods inherited from class jml2b.util.Profiler

runGC

Methods inherited from class java.lang.Object

getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Method Detail

toLang

public ITranslationResult toLang(int indent)
                          throws LanguageException

Converts the binary formula to a string suitable for output into the Java view.

• a <+ { b |-> c} is converted in a WITH b.a == c
• a <+ {b} * {c} is converted in a WITH b.a == c
• otherwise a <+ b is converted in a <+ b
• j_int2short(a) is converted in (short) a
• j_int2byte(a) is converted in (byte) a
• j_int2char(a) is converted in (char) a
• xxxelements(a)(b) is converted in a[b]
• typeof(a) is converted in typeof(a)
• otherwise a(b) is converted in b.a
• a : b is converted in b a
• a == true is converted in a
• bool(a) == bool(b) is converted in a == b
• bool(a) == false is converted in !a
• otherwise a == b is converted identically
• a <: b is converted identically
• a --> b is converted in b
• a .. b is converted identically
• a * b is converted identically
• a \/ b is converted identically
• a <| b is converted identically
• a <<| b is converted identically

Specified by:

toLang in interface ITranslatable

Parameters:

indent -

Returns:

the result of the translation.

Throws:

LanguageException