The bytecode proof obligation generator

Jack 1.8 release has an integrated compiler from the high level specification language JML to the ByteCode Specification Language (BCSL for short) and a Java bytecode verification condition generator. The verification condition generator must receive as an input a class file annotated with BCSL specification and where the bytecode is generated by a non optmising compiler.

What can it serve for?

The JML compiler and the bytecode proof obligation generator, for the moment, are in experimental phase. The final purpose is that they should allow a code receiver side to establish trust in untrusted interface implementation which potentially is not accompanied by its source code. In particular, the interface implementation side, provided with the interface specification, will annotate sufficiently the source code up to be provable against the interface specification. Once the implementation, annotation and static checking processes give the positive results, the code can be compiled; the code producer, then, generates an annotated class file, using the compiler provided by Jack as explained later; the annotated class file contains enough information, such that the client be able to establish that the bytecode respects the interface specification. In particular, the client uses the bytecode proof obligation generator in Jack as explained also later

Compiling JML annotations into Bytecode Specification annotations

First, you can look at the subset of JML keywords and operators, that the JML compiler supports. Basically, we support a light weight specification. We do not support pure method calls in specification. The JML compiler compiles the high level JML source specification into low level bytecode specification. How to do this is explained hereafter. The JML compiler does not depend on any specific Java compiler that generates debug information: the class data structures Local_Variable_Table which describes the local variables for a method and the Line_Number_Table, which describes the link between source code lines and the bytecode instructions. The Java Sun compiler by default generates those attributes. Most of the compilers support options for generating this data. Compiling JML specification into bytecode specification and inserting it in the corresponding class file involves these steps:

Generating proof obligations for annotated Java classes

Proving the proof obligations

You can see the proof obligations the generated proof obligations Start eclipse, open the Jack perspective. If you want to automatically prove a goal (i.e. a proof obligation ), then you have to : In order to prove interactively a goal, you have to do the following: