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:

Launch eclipse with the installed Jack plugin
Go to the Java perspective in eclipse
The annotated with JML java file that you want to "jml compile" must be part of an eclipse project. Position the mouse cursor over the file and click with the right mouse button and select Jack>Bytecode>Class file annotation

A class file containing the jml compilation is created and put in the directory JPOs (this directory is created by Jack in the same project where the corresponding java file is positioned) Note that the directory JPOs is not visible in the Java perspective
If you want to see the class, go to the Resource perspective. The

Generating proof obligations for annotated Java classes

Launch eclipse with the installed Jack plugin
Go to the Resource view in eclipse
Look in the file hierarchy for the annotated class file that you want to verify
Position the mouse cursor on the class file, click with the right mouse button and select the JML Compile option. A progress bar will appear.

A file with an extension .jpo and name the name of the class is created in the JPOs directory. It contains the proof obligations in the Jack internal format.

Proving the proof obligations

You can see the proof obligations the generated proof obligations Start eclipse, open the Jack perspective.

You have already generated the proof obligations for the class file
Go to the JPOs directory
Find the corresponding .jpo file

If you want to automatically prove a goal (i.e. a proof obligation ), then you have to :

Position the mouse cursor over it, right click; select Jack>Prove and select the prover(Coq, Simplify, PVS) that you want to do the automatic proof.
A window with the proof status appears

In order to prove interactively a goal, you have to do the following:

Position the mouse cursor over the goal, right click and select Jack>Edit. Eclipse will switch automatically to the Case Explorer view in the Jack perspective where the class and its method are shown. You can expand the method node and see its verification conditions

To prove a verification condition, position the mouse over it, right click with the mouse and choose Prove> and the prover in which you want to do the interactive proof.