Next: , Previous: Type Checking BML, Up: Top

9 JML to BML Compiler


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.

Except from that we use some operations which construct

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

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) =
                 translationcontext1 = ...add package information to
                 translationcontext2 = translationcontext1
                 translationcontext3 = ...add imports information to
                 Tr( getDefinition(top-level-definitions,

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) =
                  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.