9 JML to BML Compiler

We define a function Tr : JMLAST x Ctxt -> Ctxt which describes the translation of the BML to JML. This function takes as argumets an abstract syntax tree of a JML statement and a translation context and returns a new translation context which is the context from the argument enriched with the result of the translation.

The translation contexts, elements of Ctxt, are just abstract syntax trees corresponding to the grammar of the textual representations of BML Specifications (see Textual Representation of Specifications). The replace function replaces in the given translation context the item from the second argument with the item on the third argument. We use also a number of operations to retrieve the particular subtrees of the current translation context.

• getStaticInvariant : Ctxt only static invariant which is present in the context given in the parameter, in case there is no static invariant, it is undefined.
• getInvariant : Ctxt only object invariant which is present in the context given in the parameter, in case there is no object invariant, it is undefined.
• getInvExpression : Invariants -> Expressions - which retrieves from the given invariant its expression.
• getStaticConstraint : Ctxt only static history constraint which is present in the context given in the parameter, in case there is no static history constraint, it is undefined.
• getConstraint : Ctxt only object history constraint which is present in the context given in the parameter, in case there is no object constraint, it is undefined.
• getDefinition : JMLAST x ClassNames -> JMLAST the Java AST a class definition of the given name.
• getClassName : Ctxt the given context the name of the only class present in the context.

Except from that we use some operations which construct

• packStaticInvariant : Expressions -> Invariants - which constructs a static invariant out of an expression.
• packInvariant : Expressions -> Invariants - which constructs an object invariant out of an expression.
• packStaticConstraint : Expressions -> Constraints - which constructs a static constraint out of an expression.
• packConstraint : Expression -> Constraints - which constructs an object constraint out of an expression.

As some of the functions above can be undefined, we additionally define operations which take into account that possibility. We assume the following definitions

• &&^* takes two expressions and returns the expression being their conjunction; in case one of the arguments is undefined and the other defined the result is the only defined argument; in case both arguments are undefined, the result is undefined.

We start the translation with an AST of the JML-annotated class and a translation context C0 which contains the BML AST of the class:

     class Name {
     }

that means the empty class the name of which is the name of the class for which we want to obtain the translation. It is necessary to provide a name of the class as the source code files may contain several definitions of classes. The way the name is constructed is described in the section How do inner classes affect the organization of the Java Virtual Machine? of [InnerClasses-Sun97].

The definition of the translation function is the following:

     +  Tr( [package-definition] [refine-prefix] [import-definitions]
            [top-level-definitions], translationcontext) =
               let
                 translationcontext1 = ...add package information to
                                          translationcontext...
                 translationcontext2 = translationcontext1
                 translationcontext3 = ...add imports information to
                                          translationcontext2...
               in
                 Tr( getDefinition(top-level-definitions,
                                   getClassName(translationcontext)),
                     translationcontext3)

Note that BML does not handle the JML refine prefixes. To enable easy future addition of this feature, we make translationcontext2 equal to translationcontext1. We assume that the operations surrounded by ... are done by an available Java compiler infrastructure.

     ...
     +  Tr(invariantkeyword predicate, translationcontext) =
          replace(translationcontext,
             getInvariant(translationcontext),
             packInvariant(
                getInvExpression(
                  getInvariant(translationcontext)) &&^*
                getExpression(Tr(predicate, translationcontext ))))

See Mariela's documents Compiling Java Modeling Language Specification, in particular Section 5 and further, and Java Bytecode Specification and Logic, in particular Section 2.6.