Next: Acknowledgements, Previous: Relation with JML, Up: Introduction
[Update]
Development of tools for BML is part of the development of the Mobius tool set. We are currently working on a viewer for BML annotations. Eventually, this viewer should also be usable to write BML specifications directly at bytecode level.
The verification condition generator uses a translation of BML-annotated bytecode files into the BoogiePL language [DeLine-Leino05]. This translation has been proven sound [LehnerM07]. A verification condition generator for BoogiePL can then be used to generate the appropriate proof obligations.
A prototype compiler from JML to BML specifications exists; it is future work to extend this to the complete BML language as defined in this manual.
BML in its current form does not support the specification of resource properties, or the verification of multithreaded programs. Support for this is developed in independent branches of the Mobius project. However, whenever appropriate verification techniques exist, because of the close correspondence with JML, it is fairly easy to integrate these into BML, provided the verification techniques for source code and bytecode match appropriately.
Additionally, BML does not cover the issues associated with inner and anonymous classes. These features are notoriously difficult to understand and special care would be needed to incorporate these in BML in the right way.