Contracts for Java Bytecode

Question

Introduction
For a paper I need contracts, which are also referred to as Design by Contract (DbC)1, and conceptually go back to Hoare[2]. For my work I need to apply contracts to Java bytecode. The question is only about using contracts on Java bytecode, nothing more.

If you ask, why do you want to use contracts on Java bytecode, there is a reason. The reason is that I use a Java extension. This Java extension takes source code consisting of extended Java code, from which it generates bytecode. I want to use this Java extension and additionally I want to use contracts. The extension doesn't support contracts. So I have my extended Java code, I apply to it the compiler of the Java extension and I get Java bytecode. On this resulting bytecode I want to apply contracts.

The Java extension is called Object Teams[4], also called eclipse object teams. The Java extension allows to use dynamic collaborations and aspects, which are not part of regular Java code.

Right now I only need a hack or workaround to get one or two small examples working.

My idea so far:
This is irrelevant to the question. But it shows that my current plan is cumbersome and I need a better solution (thus the question). Also, perhaps someone has worked with JML/OpenJML and might know how to do this plan but better.

There is a tool for contracts for Java language. The tool is called java modeling language(JML)[3][5]. The tool does not support contract for Java bytecode. The tool only supports contracts on Java source code. I want to rewrite part of the tool to support contracts on java bytecode (a solution to my question but a cumbersome one).

Currently there is only one working version of the java modeling language(JML), which is called OpenJML[6]. I plan to use OpenJML on Java bytecode (remember, OpenJML doesn't support contracts for bytecode, only contracts for Java source code). I don't want to use contracts on any bytecode. I want to use contract on bytecode that is generated by a Java extension. (The Java extension is called ObjectTeams, but this is irrelevant for the question).

(Annotations mean annotations that are part of the Java language, e.g., "@Overrides".)

The approach would be to search for specific annotations in the bytecode that is generated by a Java extension. Those specific annotations specify contracts. I have to look for the specific annotations in the bytecode (bytecode that is generated by a Java extension), compile them to Java guard expressions, i.e., code that throws an exception if the contracts are not honored. I can get the compiled Java guard expression by using the library behind OpenJML. Then I need to add the byte code of the Java guard expression at the place where I found the specific annotations that represent contracts.

My question:
Using OpenJML seems possible, but difficult to achieve. Right now I just need a solution that works for one or two small examples, so the solution can be a hack or just a temporary solution. As my approach via OpenJML is probably difficult to achieve and further will take quite some time, I look for different solutions.

Question: What options would you recommend to apply contracts (design by contract) for java bytecode?

Requirements:

1. a up to date tool or library (i.e., not a project where development has ceased or stopped three years ago)
2. ideally, it should be straightforward to use the tool or library (i.e., not a project with zero or almost no documentation)

--

---

Update / Clarification:

• I forgot to mention that don't need any form of static checking. I
  only need to check that the contracts hold during run time. Further I only need to use very basic contracts (pre- and postcondition,
  invariants) applied to only a few methods of my program.
• As Dave as pointed out in the comments, there may be another option to apply contracts together with Object Teams. This would mean modifying or extending Object Teams and the CoreJDT module of Object Teams (it's in the comments).
• I also got a reply from the creator of Object Teams that using JML and Object Teams together via JDT isn't an easy fix.

References:

1 B. Meyer. Applying Design by Contract. Computer, 25(10):40{51, 1992.

[2] C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica, 1(4):271–81, 1972.

[3] Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael Ernst, Joseph R.Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll. An overviewof JML tools and applications. International Journal on Software Tools for Technology Transfer (STTT), 7(3):212–232, 2005.

[4] http://www.eclipse.org/objectteams/

[5] http://www.eecs.ucf.edu/~leavens/JML//index.shtml

[6] http://jmlspecs.sourceforge.net/

Answer 1

I recommend you look at BML. It is like JML, but for Java bytecode. It allows you to specify contracts (preconditions, postconditions, data structure invariants) at the bytecode level. I think the tools Umbra, JACK, and the Mobius program verification environment support BML, and the Mobius project is building tools that work with BML. See, e.g., the following papers:

• BML and related tools. Jacek Chrzaszcz, Maricke Huisman, ALeksy Schubert. FMCO 2008.

• Verification and certification of Java classes using BML tools. Jacek Chrzaszcz, Aleksy Schubert, and Tadeusz Sznuk.

• Preliminary Design of BML: A Behavioral Interface Specification Language for Java bytecode. Lilian Burdy, Marieke Huisman, and Mariela Pavlova. FASE 2007.

• Technical Aspects of Class Specification in the Byte Code of Java Language. Aleksy Schubert, Jacek Chrzaszcz, Tomasz Batkiewicz, Jaroslaw Paszek, Wojciech Was. Elsevier Science.

• JACK: a tool for validation of security and behaviour of Java applications. Gilles Barthe, Lilian Burdy, Julien Charles, Benjamin Gregoire, Marieke Huisman, Jean-Louis Lanet, Mariela Pavlova, and Antoine Requet. FMCO 2007.

You might also look at BCSL and JVer, which are intended for verifying Java bytecode, and JML2BML, which translates JML to BML:

• Java Bytecode Specification and Verification. Lilian Burdy, Mariela Pavlova.

• JVer: A Java Verifier. A Chander, D. Espinosa, N. Islam, P. Lee, G. Necula. CAV 2005.

• Supplementing Java Bytecode with Specifications. Jedrzej Fulara, Krzysztof Jakubczyk, and ALeksy Schubert.

You might also want to ask on the JML mailing list, as they might have other recommendations/suggestions.

Other possibly related work: JINJA (Tobias Nipkow), Claire Quigley's work. And, you might look at the proceedings of the BYTECODE workshop over the past decade, as it presents research on verification and analysis of bytecode (including Java bytecode).

Caveat/disclaimer: Be warned that you might not find an equivalent of JML for Java bytecode that's as convenient and easy-to-use and well-supported as JML. The reason is that contracts are designed to be used and understood by programmers. The natural place to put contracts is on the source code, because that's a lot easier for programmers to use; putting contracts on bytecode is a more niche requirement.