Next: Bibliography, Previous: JML to BML Compiler, Up: Top
Static verification of BML specifications can be defined in two different ways: via a translation into an intermediate format, or via the definition of a so-called direct verification condition generator (direct VCGen). The use of an intermediate format has the advantage that proof obligations can be kept small, and tools can be efficient. The use of a direct VCGen has the advantage that the link between proof obligation and annotated program is directly available. Moreover, because of the close correspondence between Java source code and bytecode, a direct VCGen makes compilation of proofs straightforward.
[MH260908: are there more (dis)advantages we should add here?]
This chapter defines a translation of BML into the BoogiePL intermediate format [DeLine-Leino05]. This language is also used as intermediate format for the verification of Spec# programs. Different implementations of verification condition generators exist for Boogie (from the Spec# team, and FreeBoogie [Grigore08]). The translation is an extension of the translation presented by Mallo [Mallo07], covering all language constructs present in BML. Mallo, building on earlier work of Suzuki [Suzuki06] presents a translation from Java bytecode into BoogiePL. We do not discuss this translation further here; we simply assume this as given. In addition, Mallo describes how BML lightweight specifications (containing requires, ensures, assignable and signals clauses only), loop specifications, class invariants and ghost fields are translated into BoogiePL. In this chapter, we summarise his translation, and extend it to full BML.
Pavlova [Pavlova07] has presented a direct VCGen for a subset of BML. In addition, she has proven soundness of this VCGen.
[MH260908: should we have one BML AST format, that is used as target for JML2BML compiler, and source for verification?]
[MH260908: I did not check the correct BoogiePL syntax, eg. for not, conjunction and disjunction. This still has to be done.]