Supplementing java bytecode with speci cations

Abstract. The proof-carrying code (PCC) techniques allow the exe-cutable code to be augmented with a proof that the code obeys certain policies (e.g. the program does not store passwords in clear in a file). BML (Bytecode Modelling Language) can be regarded as a part of the PCC architecture which allows to express detailed properties of Java bytecode programs. As most of the programming is done at the source code level, it is desirable to have a way to translate properties expressed at the source code level (in our case written in Java Modeling Language, JML) to the bytecode level. In this paper we present a JML2BML com-piler, a tool that for a given Java source file annotated with specifications generates class files with BML.