IntroductionFor 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:  a up to date tool or library (i.e., not a project where developmenthas ceased or stopped three years ago)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. Ionly need to check  that the contracts hold during run time. FurtherI 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 optionto apply contracts together with Object Teams. This would meanmodifying or extending Object Teams and the CoreJDT module of ObjectTeams (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):27181, 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):212232, 2005.[4] http://www.eclipse.org/objectteams/ [5] http://www.eecs.ucf.edu/~leavens/JML//index.shtml [6] http://jmlspecs.sourceforge.net/
Contracts for Java Bytecode
programming languages;formal methods;object oriented;java