9 JML to BML Compiler

[Aleksy]

We define a function Tr : JMLAST x Ctxt -> Ctxt which describes the translation of the JML to BML. 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 a copy of the context in the argument augmented with a direct tranlation of the JML expression. 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). We define the translation in this way as results of some translation operations must be `attached' to certain existing nodes.

This update is done using a replace function. The replace function replaces in the translation contextin the first argument the node from the second argument with the node on the third one. 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.