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:
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));
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):
assert not (f=null); assume not (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 (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.
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?e2e3) = ?? (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(e1instanceofT) = 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.
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:
assert Tr(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:
assume Tr(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:
assert false;
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):
assert not (l=null); assume not (l=null);
No translation defined for the ownership modifiers for the moment.