Home Java Cofoja: A practical library for contract programming.Part 1

Cofoja: A practical library for contract programming.Part 1

by admin

This article is a translation of the document "2010 internship technical report" Cofoja library. The paper reveals the origins of the library and answers critics’ questions that can be found on Habra in articles about the library. The article serves to disseminate and understand implementations of the Design By Contracts or Contracted Programming paradigm.
This article is divided into two parts due to the amount of translation work. The second part will appear soon.
Contents
Quick review
1 Introduction
2 Contract annotations
3 Components and Architecture
4 Compilation of the contractual aspect
4.1 Compiling the Board
4.2 Connection points and binding
4.3 Inheritance of the Board
4.4 Limitations of the Compilation Technique
5 Contract Life Cycle
5.1 Close-up on the Compilation of the Contract
5.2 Layout of the Contract Method
5.2.1 Classes and interfaces
5.3 Runtime Behaviors of a Contract
5.3.1 Contract recursion
5.4 Special case of Old-value expression
6 Discussion
7 Conclusion
8 Acknowledgements
List of references cited


Nhat Minh Le
January 12, 2011

Short review

This article introduces Contracts for Java (Cofoja), the new library for contract programming in Java and the successor to Modern Jass (Johannes Rieken). The library improves on its predecessor’s strategy, which is based on a separate compilation stubs ), although it uses the same Java technologies, such as annotation processing and bytecode instrumentation.
Contracts for Java promotes minimalism with an expressive set of constructs, reminiscent of the original Design By Contract idea pioneered by the Eiffel language, which allows you to focus on reliability, execution and enforced unobtrusiveness during compilation.

Introduction

Contract programming is a paradigm for building object-oriented software that was first described by Bertrand Mayer and spread through his Eiffel programming language with built-in Design By Contract constructs. In essence, it extends the relations of the class hierarchy with software-enforced constraints called contracts. In Meyer’s original proposal, they were expressed as a method of preconditions and postconditions, similar to Hoar logic. and class invariants, which act as both preconditions and postconditions to all interfaces of the class. Contracts can be inherited according to the Barbara Liskova’s substitution principle
While contract programming won great success in its original implementation of the Eiffel language, where it is respected as a fundamental idiom, it has been exported and adapted with various levels of success into other languages, including Java.
Contracts in Java rely on third-party libraries since the language itself only includes underdeveloped assertion support like Java 6. Numerous efforts have brought a dozen alternatives over the years, such as JML, C4J, Contract4J, JASS and the previously mentioned Modern Jass, on which Cofoja is based.
Cofoja has collected everything known before and improved interesting approaches that were introduced separately in the mentioned libraries, in order to create a stable independent library specialized on contract programming in Java:

  • Brief contract specification using Java annotations (Contract4J, Modern Jass)
  • Full support for Java expressions in a contract, using the accompanying compilation through a standard compiler API (Modern Jass)
  • Check at compile time of syntax and types (no interpretation at run time of contract expressions, like Contract4J)
  • Online and offline binding of contracts to target objects, using bytecode rewriting. (C4J, Contract4J, Modern Jass)
  • And lightweight code is based on few dependencies (in particular, there is no dependency with AspectJ as in the case of Contract4J)

The main contribution of this implementation is an advanced version of the model compilation presented in Modern Jass, inspired by AOS techniques and based on the use of the Java compiler standards, producing stubs and imaginary objects (mocks)
Sections 2 and 3 describe an overview of the Cofoja library and its use, and sections 4 and 5 cover the details of the contract presentation, the implementation of the contracts themselves from the inside.

2 Contract annotations

All Cofoja constructs are expressed through a small set of Java annotations : Reuires, Ensures, Invariant, directly borrowed from Eiffel, and the less used ThrowEnsures and Contracted. The first four annotations are typed to define contracts as lists of statements (see Fragment 1)

 <code>@Invariant("size() > = 0")interface Stack<T> {public int size();@Requires("size() > = 1") public T peek();@Requires("size() > = 1")@Ensures({"size() == old(size()) - 1", "result == old(peek())"})public T pop();@Ensures({"size() == old(size()) + 1", "peek() == old(obj)"})public void push(T obj);}</code> 

Fragment 1: Example contract stack.
As in Eiffel, contracts can be inherited by making fragments of inheritance chains using AND and OR Boolean operators.
These annotations provide a complete set of basic contract specifications on top of which it is easy to construct more complex behaviors. In fact, statements can contain arbitrary Java expressions, i.e., any check written in Java can be written in Cofoja contract.
Cofoja, as defined in its goals, does not seek to provide the innovative and specialized functionality that has been introduced in packages such as JML and JASS. Instead, it focuses on the usability and accessibility of its core features. Even adding a small functionality to a whole array of constructs in an existing language such as Java is a tried and tested challenge and previous attempts at contractual programming libraries for Java often ended up with partial support for contractual features : for example, JML only learned the limits of Java 5 despite efforts to bring everything up to date; Modern Jass fails when compiling code with generalized types and libraries that refrain from manipulating code or bytecode can only commit
One of the goals of Cofoja is to bring contracts to as many variations of Java code as possible, with expressiveness on ease and recoverability. The following articles describe the fundamental techniques that lie in the implementation of contracts in Cofoja. Supporting features, such as debugging, are only mentioned in appropriate places and deserve a study in their own right, which is outside these articles.

3 Components and Architecture

Cofoja: A practical library for contract programming.Part 1
Excerpt 2: Compilation and Deployment Process
Fragment 2 describes the compilation and execution process when Cofoja contracts are enabled. Contracts are integrated at different entry points, using the Java toolchain, and at both compile time and runtime :

  1. Before compiling Java, as only-reads the source by the preprocessor. It is important to note that this step does not modify the source files; its exclusive purpose is to pull out information that cannot otherwise be accessed in the handler annotations (see below). The preprocessor is not needed if the Java compiler has a non-standard API with the com.sun.source package
  2. When compiling Java files, as annotation processor. The annotation processor is responsible for the ongoing compilation of contract code into individual bytecode files.
  3. During class loading, as the Java agent, a plugin for the Java program launcher module. The Java agent rewrites the bytecode of the contract classes, connecting the contracts to the target objects.
  4. Optional step. A toolkit step that can be performed outside of running Java programs as an independent process that combines normal contract-free bytecode (in the form of standard class files) with the corresponding contract bytecode (in the form of contract files) to synthesize classes with valid contracts.

Cofoja also comes with two utilities : cofojac and cofojab which performs the first two steps and the last step, respectively, for easy execution from the command line.
The key idea, taken from Modern Jass, is to compile the contracts separately. The original source files are never changed anyway. It has disadvantages, mostly syntactic (e.g., contract code is written inside double quotes), but guarantees the following two properties that contribute to this approach reliability :

  • Contract compilation does not overlap with the normal compilation process; this limits the potential for bugs in contract compilation, using the compiler’s intended behavior of the original code.
  • The contract compiler does not need contracted code to compile; annotated code layout is sufficient. If for some reason (such as a bug in a library or unsupported Java functionality) Cofoja cannot be used on a specific piece of code, then you can still continue development, leaving contracts selectively or for a while.

Contracts are immediately attached to classes after they have been processed, and so their original representation as inert data (e.g. string literals), go through many forms during their lifetime. The following sections describe how contracts are translated from their specifications into valid bytecode. Section 4 describes a general compilation technique borrowed from AOP, while Section 5 describes the internal implementation in Cofoja.

4 Compilation of the contractual aspect

Contract checking is created by crosscutting in code, if described in aspect-oriented terms. Although contracts themselves define the business logic properties of a program, checking them is represented as Application Aspects.
Confirmation or failure of the invoked code can be naturally expressed as a Tip regarding contractual methods. The Modern Jass library has introduced a new stub-based compilation technique and the use of the standard Java compiler to generate Advice into bytecode, which can later be linked through the Java agent toolkit. This approach has the advantage of doing away with an additional compiler with its understanding of the Java language. It does, however, tightly bind the code to the contract logic.
Cofoja has improved this approach by extending the compilation process to systematic constructs that display more transparently aspectual concepts.

4.1 Compilation of the Council

The main problem in compiling Board code lies in code that requires access to the same environment as the method to which the Board applies. In other words, the Board part expects to be compiled as if it were inside the same boundaries as the code being modified. A precondition, for example, probably checks the call arguments or any contract may want to call a private method of a class. This is easily achieved if the compiler is aware of it; standard Java compiler, however, does not pay attention to them.
To do this, the Java compiler is used in this order: the board is injected back into the copy of the original class, turning it into byte code and then the resulting compiled methods are extracted. These methods can easily be linked inside the final classes (as additional methods) until they are loaded. Thus, the bytecode belongs to the optional aspect, moreover, it is compiled and stored separately and fully reusable.
The technique has improved, so that methods of the original class can be replaced by stubs. What is important is that the compiler properly generates calls to these methods inside the Board Code; and their actual contents are unimportant. In this regard, the standard annotation processing API provides sufficient information to easily generate stubs by reflecting elements of the class hierarchy. An additional benefit is the class applicability extensions available only as bytecode: method signatures can be read from class files, ignoring associated method bodies.

4.2 Connection points and binding

Binding is completed through rewriting the bytecode : additional methods are added to the class and methods to which the Tips are applied are supplemented by calls to them at the beginning and at the output of the method.
Temporary data such as arguments and return value, if any, must be copied explicitly as if they were implicitly moved from method to method.
In addition to this, parts of the Council that surround a method and have post-conditions with old-value expressions are trivial, but special cases for which you need to preserve context. In Cofoja, the solution to preserve context is done by setting additional local variables that are added to the post-value signature of the Council method.
Contracts are particularly well suited for this approach, since the information context is naturally split into a set of non-overlapping variables. Two alternatives: embedding inside Council byte-code methods and splitting method-Council inside an auxiliary entity.
Embedding inside methods is an attractive solution if the Board code is not inherited or ensures that any private members of ancestor classes are not accessed. Otherwise, embedding breaks the advantages of access boundaries.
A more general strategy is to place a helper method inside a helper, which consists of the actual code, and a wrapper, which borrows the original name and signature of the original, but its actual work is subordinate to the helper methods, which are responsible for calling the helper procedure.

4.3 Council Inheritance

Inheritance is a central part of the Contract paradigm. But it is largely orthogonal to AOP. With this approach, it should be clear that methods-Counsels are naturally inherited through a normal class hierarchy and they are available during binding. With some extra effort, they can also be accessed with source code.
Depending on the application, an inherited Board can greatly change its very nature and purpose, different strategies are possible, but that is beyond the scope of this document.
Nevertheless, an issue arises when using the interface. It should be noted that writing the Council for an interface is an important part if there is a way to connect these pieces inside the specific classes that implement that interface. Obviously, there is no way to inject the Aspect code inside the original interface; the resulting Java file will not even compile and this defeats the purpose of this technique.
Instead, additional methods can also live in a particular class implementing a single interface or in a utility class within the same boundaries as the interface to which they are attached (same package or outer-class).
The first solution is to use the existing linked infrastructure: the classes implementing the interface can easily attach methods-counsels and continue to exist as usual. Nevertheless, care must be taken to turn all references to the implemented class into references of the actual class whose methods are injected. There are also problems with duplicate code.
The second solution requires that chunks of the Board for the interface be redone to work with an additional parameter acting to control the actual object. Nevertheless, this eliminates any duplication. Note that the reliance on external procedures does not limit the expressiveness of these constructs, since interfaces only have public constructs.
Section 5.2.1 addresses these problems from a Contracts practice perspective : it compares an implementation of Modern Jass, which uses a variant of the first solution, and Cofoja, which applies the second solution.

4.4 Limitations of the Compilation Technique

This Aspect compilation approach holds to the guarantee that the Java compiler does not optimize a method within its bounds. In fact, it requires that source code methods and bytecode methods combine one-to-one, e.g., no method splitting at compile time. In the presence of stubs, embedding a piece of method directly is the other big undesirable optimization. In practice, this is not much of a problem, given the current trends toward virtual machine-level optimization than compiler-level optimization. Also, Contracts in particular are designed primarily for development and debugging purposes, and therefore probably won’t compile with optimization included.
Another possible more serious problem is compilation errors. Error reporting requires more care because it tends to produce elusive inconsistencies. A simple idea is to give the result from the main compiler process, so that the user is shown the generated messages, not related to the user code, but corresponding to the mixed code with the generated elements. Cofoja supplements such an option with advanced features to help clarify common error messages; a more general solution could use improved integration with the compiler API.

List of references

You may also like