April 4, 2012 at 11:46

Cofoja: A practical library for contract programming. Part 1

    This article is a translation of the 2010 internship technical report of the Cofoja library. The document reveals the reasons for the emergence of the library and answers the questions of critics that can be found on Habré in articles devoted to this library. This article serves to disseminate and understand implementations of the Design By Contracts or Contract Programming paradigm.

    The article is divided into two parts in relation to the amount of translation work. The second part will appear shortly.

    Contents

    Overview
    1 Introduction
    2 Contract annotations
    3 Components and Architecture
    4 Compilation of the contract aspect
    4.1 Compilation of the Council
    4.2 Connection points and binding
    4.3 Inheritance of the Council
    4.4 Limitations of the Compilation Technique
    5 The life cycle of the Contract
    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 Behavior of the Contract at Runtime
    5.3.1 Contract Recursion
    5.4 Special Case of Old-value Expressions
    6 Discussion
    7 Conclusion
    8 Acknowledgments
    Cited List literature


    Nhat Minh Le
    January 12, 2011

    Short review

    This article introduces Contracts for Java (Cofoja), the new library for Java contract programming and the successor to Modern Jass (Johannes Rieken). The library improves the predecessor strategy based on a separate compilation of 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, which is pioneered by the Eiffel language, which allows you to focus on reliability, execution and enforced unobtrusiveness in the compilation process.

    Introduction


    Contract programming is the paradigm of building object-oriented software, which was first described by Bertrand Mayer and spread thanks to his Eiffel programming language with built-in Design By Contract constructs. Essentially, this extends the class hierarchy relationship with software-constrained constraints called contracts. In Mayer's original sentence, they were expressed as a method of preconditions and postconditions, similar to Hoare logic and class invariants that act as both preconditions and postconditions to all class interfaces. Contracts can be inherited in accordance with the principle of substitution Barbara Liskova .

    While contract programming has gained 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 to other languages, including Java.

    Contracts in Java rely on third-party libraries because the language itself only includes underdeveloped support for assertion like Java 6. Numerous efforts have brought a dozen alternatives in recent years, such as JML, C4J, Contract4J, JASS and the previously mentioned Modern Jass, on which Cofoja is based.

    Cofoja compiled everything that was known earlier and improved interesting approaches that were introduced separately in the mentioned libraries in order to create a stable independent library specialized in contractual programming in Java:
    • Brief contract specification using Java annotations (Contract4J, Modern Jass)
    • Full support for Java expressions in the contract, using concomitant compilation through the standard compiler API (Modern Jass)
    • Checking syntax and types at compile time (no interpretation at runtime of contract expressions like Contract4J)
    • Online and offline binding of contracts to targets using rewriting bytecode. (C4J, Contract4J, Modern Jass)
    • And the lightweight code is based on a small number of dependencies (in particular, there is no dependency with AspectJ as in the case of Contract4J)

    The main contribution of this implementation is an improved version of the compilation of models presented in Modern Jass, inspired by AOP techniques and based on the use of Java compiler standards, producing stubs and imaginary objects (mocks)

    Sections 2 and 3 describe the overview of the Cofoja library and its use, and sections 4 and 5 cover the details of the presentation of contracts, the implementation of the contracts themselves from within.

    2 Contract annotations


    All Cofoja constructs are expressed through a small set of Java annotations: Reuires, Ensures, Invariant, directly borrowed from Eiffel, and less used ThrowEnsures and Contracted. The first four annotations are printed to define contracts as lists of statements (see snippet 1)
    
@Invariant("size() >= 0")
interface Stack {
	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);
}

    Fragment 1: An example of a stack with contracts.

    As with Eiffel, contracts can be inherited by composing fragments of inheritance chains using AND and OR Boolean operators.
    These annotations provide a complete set of basic contract specifications at the top of which it is easy to build more complex behaviors. Actually, statements can contain arbitrary Java expressions, i.e. any validation written in Java can be written in the Cofoja contract.

    Cofoja, as defined for its purpose, does not seek to provide the innovative and specialized functionality that has been introduced into packages such as JML and JASS. Instead, it focuses on usability and accessibility of its core capabilities. Even adding small functionality to an entire array of constructs in an existing language such as Java is a tried and tested task, and previous attempts at Java contract programming libraries often ended up partially supporting contractual capabilities: for example, JML only got to know the limits of Java 5 despite the effort to bring everything to time; Modern Jass fails when compiling code with generic types, and libraries that refrain from manipulating code or bytecode can only accept interface obligations.

    One of Cofoja's goals is to bring contracts to as many variations of the Java language code as possible, with expressiveness for ease and recoverability. The following articles describe the fundamental techniques that lie in the implementation of contracts at Cofoja. Ancillary features, such as debugging, are only mentioned in the appropriate places and deserve independent study, which is outside of these articles.

    3 Components and Architecture



    Fragment 2: Compilation and deployment process

    Fragment 2 describes the compilation and execution process with Cofoja contracts enabled. Contracts are integrated at various entry points using the Java toolchain, both at compile time and at run time:
    1. Before compiling Java, as soon as the source is read by the preprocessor. It is important to note that this step does not modify the source files; its sole purpose is to pull out information that otherwise could not be available in the handler annotations (see below). A preprocessor is not needed if the Java compiler has a non-standard API with the com.sun.source package
    2. When compiling Java files, like annotation processor. The annotation processor is responsible for the current compilation of the contract code into separate bytecode files.
    3. During class loading, as a Java agent, a plug-in for the module for launching Java programs. The Java agent rewrites the bytecode of the contract classes, connecting the contracts to the targets.
    4. Optional step. A toolkit step that can be performed outside of the launch of Java programs as an independent process that combines a 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 existing contracts.

    Cofoja also comes with two utilities: cofojac and cofojab , which perform the first two steps and the last step, respectively, for easy execution from the command line.

    The key idea from Modern Jass is to compile the contracts separately. The original source files never change in any case. It has drawbacks, mainly syntactic (for example, the contract code is written inside double quotes), but guarantees the following two properties that reliability brings to this approach:
    • Compiling contracts does not overlap with the normal compilation process; this limits the possibility of bugs during contract compilation, using the behavior of the original code outlined by the compiler.
    • A contract compiler does not need code with contracts to compile; linking code with annotations is sufficient. If for some reason (for example, a bug in libraries or unsupported Java functionality) Cofoja cannot be used on a specific section of the code, then development can still be continued, leaving the contracts selectively or for some time.

    Contracts immediately join classes after they are processed, and therefore their original representation as inert data (for example, string literals) goes through many forms throughout life. 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 an internal implementation in Cofoja.

    4 Compilation of the contract aspect


    Validation of contracts is created by cross-cutting in the code, as described in aspect-oriented terms. Although the contracts themselves determine the properties of the business logic of the program, checking them is representable as Aspects of the application.

    Confirmation or inconsistency of the called code can naturally be expressed as advice on contractual methods. The Modern Jass library introduced a new compilation technique based on stubs and the use of a standard Java compiler to generate Tip in bytecode, which can later be linked through the Java agent toolkit. Such an approach has the advantage of dispensing with an additional compiler with its understanding of the Java language. He, however, tightly connects the code with contract logic.

    Cofoja has improved this approach by extending the compilation process to systematic constructs that display more transparently aspectual concepts.

    4.1 Board compilation

    The main problem when compiling Council code lies in code that requires access to the same environment as the method to which the Council applies. In other words, part of the Council expects to be compiled as if it were inside the same boundaries as the mutable code. The precondition, for example, probably checks the arguments of the call, or any contract may want to call the private method of the class. This is easy to achieve if the compiler knows about it; the standard Java compiler, however, does not pay attention to them.

    For this, the Java compiler is used in this order: The board is embedded back into the copy of the original class, turning into byte code and, as a result, the compiled methods are extracted. These methods can easily be bound inside the final classes (as optional methods) before they load. Thus, the bytecode belongs to an additional aspect, moreover, compiled and stored separately and fully reusable.

    The technique has been improved, so that the methods of the original class can be replaced with stubs. What is important is that the compiler properly generates calls to these methods inside the council code; and their current content doesn’t matter. In this regard, the standard annotation processing API provides sufficient information to easily formed stubs by reflected elements of the class hierarchy. An additional benefit is the extension of class applicability, available only as bytecode: method signatures can be read from class files, ignoring the associated method bodies.

    4.2 Connection Points and Linking

    The binding ends by rewriting the bytecode: additional methods are added to the class and the 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 the return value, if any, must be explicitly copied, as if they were implicitly moved from method to method.

    In addition to this, parts of the Council that surround the method and have post-conditions with old-value expressions are commonplace, but special cases for which context needs to be maintained. In Cofoja, a solution for preserving the context is made by setting additional local variables that are added to the signature of the post-execution of the Council method.

    Contracts are especially good for this approach, because the context of the information naturally breaks down into a set of disjoint variables. Two alternatives: embedding Council bytecode methods inside the method and splitting the Council method inside an auxiliary entity.

    Embedding methods inside is an attractive solution if the Council code is not inherited or guarantees that there will be no access to any private members of the ancestral classes. Otherwise, embedding breaks the benefits of access boundaries.

    A more general strategy is to place the Council method inside the helper, which consists of the actual code and the wrapper, which borrows the original name and signature of the original, but its real work obeys the Council methods that are responsible for calling the auxiliary procedure .

    4.3 Inheritance of the Council

    Inheritance is a central part of the Contract Paradigm. But this is pretty much orthogonal to AOP. With this approach, it should be clear that Council methods are naturally inherited through the normal class hierarchy and are available at the time of binding. With some extra effort, they may also be available with source code.

    Depending on the application, the inherited Council can greatly change its essence and purpose, various strategies are possible, but this is beyond the scope of this document.

    However, the question arises when using the interface. It should be noted that writing a Council for an interface is an important component if there is a way to connect these pieces into specific classes implementing this interface. Obviously, there is no way to inject Aspect code into the original interface; the resulting Java file will not even compile, and this strikes the idea of ​​this technique.

    Instead, additional methods can also live in a particular class that implements a single interface or in a utility class within the same boundaries as the interface to which they are attached (the same package or outer class).

    The first decision is to use the existing connected infrastructure: classes implementing the interface can easily attach Council methods and continue to exist as usual. However, care must be taken when converting all references to an implemented class to references to the actual class whose methods are injected. There are also tasks with code duplication.

    The second solution requires that the pieces of the Board for the interface be redone to work with an additional parameter, valid for controlling the actual object. However, this eliminates any duplication. It should be noted that the hope of external procedures does not limit the expressiveness of these structures, because Interfaces have only public constructions.

    Section 5.2.1 addresses these issues from the perspective of Contract practice: it compares the implementation of Modern Jass, which uses a variant of the first solution, and Cofoja, which applies the second solution.

    4.4 Compilation Technique Limitations

    This Aspect compilation approach rests on the assurance that the Java compiler does not optimize the method within its boundaries. In fact, this requires that the source code methods and bytecode methods are combined one-to-one, for example, there is no fragmentation of the method during compilation. With stubs, embedding directly a method piece is another big unwanted optimization. In practice, this does not present a big problem, taking into account current trends towards optimizing the level of a virtual machine than a compiler. In addition, Contracts, in particular, are intended primarily for development and debug purposes, and therefore, probably, will not be compiled with the included optimization.

    Another possible more serious problem is compilation errors. Error reporting requires more caution, as he is inclined to betray elusive contradictions. A simple idea is to return the result from the main compiler process, so that the user is shown formed messages that are not related to the user code, but correspond to a mixed code with generated elements. Cofoja complements this 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

    Tags:

    Also popular now: