The BML class level declarations are (instance and static) class
invariants, (instance and static) history constraints, represents and
initially clauses, model and ghost field declarations (with
initialization instructions), data group declarations and model
methods. Moreover, normal field declarations can be annotated with BML
modifiers that are relevant for the generation of proof obligations,
such as `non_null`

and the ownership modifiers. Mallo only
describes the translation of (instance) class invariants and ghost
field declarations.

The verification methodology for class invariants is based on the Universe system. For a detailed explanation of the translation, we refer to Mallo's thesis [Mallo07]. A visible state semantics is assumed, where essentially every pre- and post-state of a method is visible, except that the pre-state of a constructor is not visible for the object being initialized. All objects must satisfy their class invariants in all their visible states.

Concretely, if we use *inv(C)* to denote the collected invariants
of class *C* (the invariants declared in *C* and its
supertypes), then for each method *m* declared in *C*, one
must show the following:

*inv(C)*is checed in all prestates of*m*, for all instances of class*C*;*inv(C)*is checked in all poststates of*m*, for all instances of class*C*- for all loops inside
*m*, and for all objects of class*C*allocated*inside*that loop,*inv(C)*is checked at every iteration of the loop.

To represent the actual invariants, a BoogiePL predicate is introduced with the following signature:

functioninv(C :name, o:ref, h : Store)returns(bool);

Intended semantics: `inv(C,o,h)` holds whenever the invariant of
class C is satisfied by object o in heap h. To axiomatize this, the
following axiom is generated for every class *C* that is
referenced during the translation (where `C`

is the name constant
representing the type *C*, and `Tr`(*inv(C)*) denotes
the translation of the BML predicate *inv(C)* (the collected
invariant of class *C*) into BoogiePL):

axiom(forallo :ref, h : Store :: inv(`C`

, o, h) <==> (isInstanceOf(rval(o),`C`

) ==> Tr(inv(C))));

In every prestate and poststate of a method call declared in *C*,
we assert and assume that the invariant holds.

assert(forallo :ref:: inv(`C`

, o, heap));assume(forallt :name, o :ref:: inv(t, o, heap))

**[MH 260908: what is **`heap`**?? And **`loopHeap`** below??]**

Finally, at the beginning of every loop header block, the following assertion is added.

assert(forallo :ref:: !alive(rval(o), loopHeap) ==> inv(`C`

,o, heap));

No translation defined for the moment.

No translation defined for the moment.

No translation defined for the moment.

No translation defined for the moment.

No translation defined for the moment.

Declared as any field?

Ghost fields are handled like any other field in the translation and set statements are translated as normal heap updates. Thus, in particular the initialization instructions are translated into appropriate heap updates, as for normal bytecode.

No translation defined for the moment.

Treated as normal methods?

The BML modifiers that are relevant for the generation of proof
obligations are `non_null`

and `nullable`

, and the ownership
modifiers.

Every update to a (normal, ghost or model) field *f* declared
`non_null`

(or not declared `nullable`

, in case
`non_null`

is the default) is followed by an appropriate assert
and assume (where `f`

is the BoogiePL variable representing the
field *f*):

assertnot (`f`

=`null`

);assumenot (`f`

=`null`

);

No translation defined for the ownership modifiers for the moment.

Method declarations can contain BML modifiers that are relevant for
the generation of proof obligations. In particular, both the result of
the method and the method parameters can be annotated with
`non_null`

, `nullable`

and the ownership modifiers.

Further, methods can be annotated with several flat specification
cases, *i.e.*, sequences of method specification cases. Both
lightweight and heavyweight specifications are supported. Each
specification case can contain requires, ensures, signals,
signals-only and assignable clauses.

For every method parameter *p* that is declared `non_null`

(or not declared `nullable`

when `non_null`

is the default),
an extra precondition `requires `

*p*` != null`

is added to
each specification case. If the method's result is declared to be
`non_null`

(or not declared as `nullable`

when
`non_null`

is the default), an extra postcondition ```
ensures
\result != null
```

is added to each specification case. The extended
method specification is translated as defined below.

No translation defined for the ownership modifiers for the moment.

Mallo only defines the translation from BML Method Specifications into
BoogiePL for lightweight specifications. This translation is defined
in two steps: first the flat specification cases are translated into a
single specification case. This translation introduces a JML keyword
`\assigns_only`

in the postconditions (both in the normal and in
the exceptional ones). Therefore, in the translation for expressions
defined below, the `\assigns_only`

is added, compared to the
expression grammar defined above.

The translation of bytecode into BoogiePL generates special BoogiePL blocks for all normal and exceptional poststates of a method. In the blocks for normal poststates, the normal postconditions are asserted, in the blocks for exceptional poststates, the exceptional postconditions are asserted.

The translation for signals_only clauses is not defined yet.

Every method call is preceded by an assert with the method's precondition.

Finally, for the assignable clause, in every poststate (both normal
and exceptional) of the method, the following assert is added (where
`oldHeap` denotes the heap in the prestate of the method,
`heap` the current heap, and `W` the set of locations
referenced by the assignable clause):

assert(foralll : Location :: alive(rval(obj(l)), oldHeap) /\ not (l in W) ==> get(heap, l) == get(oldHeap, l));

The translation for heavyweight specifications is not yet defined.

BML expressions are an extended subset of Java expressions.
Since we do not have a translation of Java into BoogiePL readily
available, we need to define the translation explicitly on the syntax
of BML expressions as defined in BML Expressions that are Directly Inherited from JML. As explained above, in addition we need
to add a translation for `\assigns_only`

expressions.
For many of these expressions, Mallo has defined an appropriate
translation. The complete translation is expressed by function
`Tr`.

**[MH 260908: needs fixing: different handling of ors and ands]**

Remember that if *T* is a name used in the original bytecode
program, we use `T`

to denote the corresponding BoogiePL
constant.

**[MH 260908: are all cases there?]**
**[MH 260908: cases true, false, null covered by constant in
expression grammar?]**

Tr(e1`?`

e2`e3`

) = ?? (Tr(e1), Tr(e2), Tr(e3))Tr(e1`<==>`

e2) = Tr(e1) <==> Tr(e2)Tr(e1`<=!=>`

e2) = Tr(e1) <=!=> Tr(e2)Tr(e1`==>`

e2) = Tr(e1) ==> Tr(e2)Tr(e1`<==`

e2) = Tr(e2) ==> Tr(e1)Tr(e1`||`

e2) = Tr(e1) \/ Tr(e2)Tr(e1`&&`

e2) = Tr(e1) /\ Tr(e2)Tr(e1`|`

e2) = Tr(e1) \/ Tr(e2)Tr(e1`^`

e2) = Tr(e1) \/ Tr(e2) /\ (not Tr(e2) /\ not Tr(e1))Tr(e1`&`

e2) = Tr(e1) /\ Tr(e2)Tr(e1`==`

e2) = Tr(e1) = Tr(e2)Tr(e1`!=`

e2) = not (Tr(e1) = Tr(e2))Tr(e1`<`

e2) = Tr(e1) < Tr(e2)Tr(e1`>`

e2) = Tr(e1) > Tr(e2)Tr(e1`<=`

e2) = Tr(e1) <= Tr(e2)Tr(e1`>=`

e2) = Tr(e1) >= Tr(e2)Tr(e1`<:`

e2) = Tr(e1) <: Tr(e2)Tr(e1`instanceof`

T) = isInstanceOf(rval(Tr(e1)),`T`

)??Tr(e1`<<`

e2) = ??Tr(e1`>>`

e2) = ??Tr(e1`>>>`

e2) = ??Tr(e1`+`

e2) = Tr(e1) + Tr(e2)Tr(e1`-`

e2) = Tr(e1) - Tr(e2)Tr(e1`*`

e2) = Tr(e1) * Tr(e2)Tr(e1`/`

e2) = Tr(e1) / Tr(e2)Tr(e1`%`

e2) = Tr(e1) % Tr(e2)Tr((T)e) =cast(Tr(e),`T`

)Tr(+ e) = + Tr(e)Tr(- e) = - Tr(e)Tr(~ e) = ?? Tr(e)Tr(! e) = not Tr(e)Tr(e.`class`

) = ??Tr(e.#n) = ??Tr(e.`super`

(exprs)) = ??Tr(e.m(exprs)) = ??Tr(e1[e2]) = ??Tr(lv[n]) = ??Tr(m) = ??Tr(c) =`c`

//wherecis a constantTr(`super`

) = ??Tr(`true`

) = trueTr(`false`

) = falseTr(`this`

) = ??Tr(`null`

) = nullTr(`\result`

) = ??Tr(`\old`

(e)) =old(Tr(e))Tr(`nonnullelements`

(e)) = ??Tr(`\typeof`

(e)) = ??(Tr(e))Tr(`\elemtype`

(e)) = ??(Tr(e))Tr(`\type`

(T)) = ??Tr(`\forall`

...) = forall ...// ?? To be completedTr(`\exists`

...) = exists ...// ?? To be completedTr(`\cntr`

) = ??Tr(`\st`

(e)) = ??Tr(`\length`

(e)) = ??Tr(`\assigns_only(exprs)`

) = ??

For all cases marked with ?? no translation is available for the moment.

The annotation statements that are supported by BML are local ghost
variable declarations, assert, assume, set and unreachable
annotations, loop specifications. Further, normal local variable
declarations can be annotated with BML modifiers that are relevant for
the generation of proof obligations (`non_null`

, `nullable`

,
and the ownership modifiers). Finally, BML also supports a debug
annotation, but this is only relevant for run-time verification. Mallo
only describes the handling of loop specifications.

For the translation into BoogiePL, local ghost variables can be treated as any other local variable. Set annotations for local ghost variables are translated into updates of the stack.

Every assert annotation `assert e;`

is translated into a BoogiePL assert
statement:

assertTr(e);

and inserted at the appropriate position in the translation of the bytecode.

Every assume annotation `assume e;`

is translated into a BoogiePL assume
statement:

assumeTr(e);

and inserted at the appropriate position in the translation of the bytecode.

As mentioned above, set annotations are translated into normal BoogiePL updates. Set annotations that update a ghost field update the heap, set annotations that update a local ghost variable update the stack.

Every unreachable annotation is translated into a BoogiePL assert statement:

assertfalse;

and inserted at the appropriate position in the translation of the bytecode.

BML loop specifications can contain loop invariants and loop variants. Mallo defines the translation of these specifications in two steps: first the loop specifications are desugared into appropriate asserts, next the asserts are transformed into BoogiePL.

The desugaring is defined as follows. If *I* is the loop
invariant and *V* the loop variant, then at the entry point of
the loop, we add:

`// assert I;`

`// assert 0 <= V;`

Next we add an assignment to a local variable `loopVariant`

,
assigning it the value of *V*. After the loop body, just before
the loop entry point is reached again, an annotation

` ``// assert V < loopVariant;`

is added. (Notice that this translation is essentially the same as the one described in Loop Statements).

The translation to BoogiePL is now easy. First, for every loop, a
variables `loopHeap_`*i* and `loopVariant_`*i* are
declared. The variable `loopHeap_`*i* is set to the current
`heap` at the end of every block that precedes a look header
block, provided it is not in the loop. The variable
`loopVariant_`*i* is used to store the value of the loop's
variant function at the beginning of each loop iteration.
At the beginning of each loop header block, we insert assertions for
the loop invariant, and to check that the loop variant is positive. At
the end of the last block of a loop body, an assertion is added to
check that the loop variant has indeed decreased (by comparing it with
`loopVariant_`*i*).

For more information, we refer to Mallo [Mallo07].

The BML modifiers that are relevant for the generation of proof
obligations are `non_null`

and `nullable`

, and the ownership
modifiers.

Every update to a (normal or ghost) local variable *l* declared
`non_null`

(or not declared `nullable`

, in case
`non_null`

is the default) is followed by an appropriate assert
and assume (where `l`

is the BoogiePL variable representing the
local variable *l*):

assertnot (`l`

=`null`

);assumenot (`l`

=`null`

);

No translation defined for the ownership modifiers for the moment.