Technical Aspects of Class Specification in Java Byte Code 1

Bytecode Modeling Language (BML) is a recent specification language designed to support specification and verification of Java byte code files. We present an editor called Umbra for byte code files which supports the editing of BML specifications. This editor is accompanied by a library BMLlib which not only parses textual representations of BML specifications and prints the specifications in a textual form, but also writes specifications into Java class files and reads them from that format. The whole tool set allows to insert BML specification into class files or inspect class files with BML specifications and edit them, e.g., for debugging purposes