Next: , Previous: Typechecking BML, Up: Top

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.

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.