4
$\begingroup$

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/

$\endgroup$
  • $\begingroup$ please give me feedback if something is not clear enough. also I am in a different time zone than most users, so my answers might take much longer than is expected $\endgroup$ – mrsteve Jul 7 '13 at 3:33
  • $\begingroup$ Is the idea that you want to compile contracts available in ObjectTeams into bytecode? $\endgroup$ – Dave Clarke Jul 7 '13 at 6:40
  • $\begingroup$ no, I just want to use contracts on bytecode. Nothing more. (just as an explanation, to why I want to do this: ObjectTeams generates bytecode. ObjectTeams doesn't support contracts. ObjectTeams only can generate bytecode from ObjectTeam source code. The only way to use ObjectTeams is to work with the bytecode that it generates. I want ObjectTeams+Contracts, the only option is to use contracts on the bytecode that ObjectTeams generates from ObjectTeams source code.) $\endgroup$ – mrsteve Jul 7 '13 at 8:25
  • $\begingroup$ @Dave: I tried to improve my question. Is it clearer now? Do I need to clarify something more? $\endgroup$ – mrsteve Jul 7 '13 at 8:55
  • $\begingroup$ I fail to understand that the only way to use contracts in ObjectTeams is to have them on the bytecode. (Also, see: jcontractor.sourceforge.net/doc/jContractor_FMSD03.pdf) $\endgroup$ – Dave Clarke Jul 7 '13 at 10:09
3
$\begingroup$

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:

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

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.