Previous: Static Verification of BML Specifications, Up: Static Verification of BML Specifications


10.1 The translation from BML into BoogiePL

10.1.1 Translation of BML Class Level Specifications into BoogiePL

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.

10.1.1.1 Instance Class Invariants

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:

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

     function inv(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 (forall o : 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(forall o : ref :: inv(C, o, heap));
     assume(forall t : 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(forall o : ref :: !alive(rval(o), loopHeap) ==> inv(C,o, heap));
10.1.1.2 Static Class Invariants

No translation defined for the moment.

10.1.1.3 Instance History Constraints

No translation defined for the moment.

10.1.1.4 Static History Constraints

No translation defined for the moment.

10.1.1.5 Represents Clauses

No translation defined for the moment.

10.1.1.6 Initially Clauses

No translation defined for the moment.

10.1.1.7 Model Fields

Declared as any field?

10.1.1.8 Ghost Fields

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.

10.1.1.9 Data Groups

No translation defined for the moment.

10.1.1.10 Model Methods

Treated as normal methods?

10.1.1.11 BML Modifiers of Field Declarations

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):

     assert not (f = null);
     assume not (f = null);

No translation defined for the ownership modifiers for the moment.

10.1.2 Translation of BML Method Specifications into BoogiePL

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.

10.1.2.1 BML Modifiers of Methods and Method Parameters

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.

10.1.2.2 BML Method Specifications

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 (forall l : 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.

10.1.3 Translation of BML Expressions into BoogiePL

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 //where c is a constant
     Tr(super) = ??
     Tr(true) = true
     Tr(false) = false
     Tr(this) = ??
     Tr(null) = null
     Tr(\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 completed
     Tr(\exists ...) = exists ... // ?? To be completed
     Tr(\cntr) = ??
     Tr(\st(e)) = ??
     Tr(\length(e)) = ??
     Tr(\assigns_only(exprs)) = ??

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

10.1.4 Translation of BML Annotation Statements into BoogiePL

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.

10.1.4.1 Local Ghost Variable Declarations

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.

10.1.4.2 Assert Annotations

Every assert annotation assert e; is translated into a BoogiePL assert statement:

     assert Tr(e);

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

10.1.4.3 Assume Annotations

Every assume annotation assume e; is translated into a BoogiePL assume statement:

     assume Tr(e);

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

10.1.4.4 Set Annotations

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.

10.1.4.5 Unreachable Annotations

Every unreachable annotation is translated into a BoogiePL assert statement:

     assert false;

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

10.1.4.6 Loop Specifications

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].

10.1.4.7 BML Modifiers for Local Variable Declarations

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):

     assert not (l = null);
     assume not (l = null);

No translation defined for the ownership modifiers for the moment.