patternjavaMinor
Contracts for Java Bytecode
Viewed 0 times
contractsbytecodeforjava
Problem
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 e
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 e
Solution
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.
-
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.
Context
StackExchange Computer Science Q#13121, answer score: 3
Revisions (0)
No revisions yet.