Geekly Articles each Day
⬆️ ⬇️

Cofoja: A practical library for contract programming. Part 1

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



The article is divided into two parts due to the amount of translation work. The second part will appear soon.



Content



Short review

1. Introduction

2 Contract annotations

3 Components and Architecture

4 Compiling the contractual aspect

4.1 Compilation of the Council

4.2 Connection points and linking

4.3 Board Inheritance

4.4 Limitations of the Compilation Technique

5 Contract Life Cycle

5.1 Close-up to the compilation of the Contract

5.2 Planning of the Contract Method

5.2.1 Classes and Interfaces

5.3 Conduct of the Contract at runtime

5.3.1 Contract recursion

5.4 Special case Old-value expressions

6 Discussion

7 Conclusion

8 Thanks

List of references

')



Nhat minh le

January 12, 2011



Short review


This article introduces Contracts for Java (Cofoja), a new library for contract programming in Java and the successor to Modern Jass (Johannes Rieken). The library improves the predecessor strategy based on separate stub compilation), although it uses the same Java technologies, such as annotation processing and bytecode instrumentation.



Contracts for Java promotes minimalism with an expressive set of constructions, reminiscent of the original idea of ​​Design By Contract, the pioneer of which is the Eiffel language, which allows you to focus on reliability, execution and forced unobtrusiveness in the compilation process.



Introduction



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



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 different levels of success to other languages, including Java.



Contracts in Java rely on third-party libraries, because the language itself only includes underdeveloped assertion support as 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 collected all the known earlier and improved interesting approaches that were introduced separately in the mentioned libraries in order to create a stable independent library specialized in contract programming in Java:



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



Sections 2 and 3 describe the review of the Cofoja library and its use, while sections 4 and 5 cover the details of the presentation of contracts, the implementation of 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 less useful ThrowEnsures and Contracted. The first four annotations are printed to define contracts as sentence lists (see excerpt 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 of a stack with contracts.



As in Eiffel, contracts can be inherited, making up 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 build more complex behaviors. In fact, 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 innovative and specialized functionality that has been introduced into packages such as JML and JASS. Instead, it focuses on the usability and accessibility of its core capabilities. Even adding a small functionality to a whole array of constructs to an existing language such as Java is a challenging task and previous attempts to contract programming libraries for Java often resulted in partial support for contract capabilities: for example, JML only got to know the limits of Java 5 despite efforts to bring all time; Modern Jass fails when compiling code with generic types and libraries that refrain from manipulating code or bytecode can only assume the obligations of interfaces.



One of Cofoja’s goals is to add contracts to as many as possible a variation of the Java language code, 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 the appropriate places and deserve self-study, which is outside of these articles.



3 Components and Architecture





Fragment 2: Compilation and Deployment Process



Fragment 2 describes the process of compiling and executing with the included Cofoja contracts. Contracts are integrated at various entry points using Java chain tools (toolchain), both at compile time and at runtime:

  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 exclusive purpose is to pull out information that could not otherwise be available in the handler's 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 like annotation processor. The annotation processor is responsible for the current compilation of the contract code into separate byte-code files.
  3. During class loading, as a Java agent, a plugin for the Java program launcher. The Java agent rewrites the bytecode of the contract classes, connecting the contracts with the target objects.
  4. Optional step. A tooling step that can be performed outside of the launch of 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 perform the first two steps and the last step, respectively, for easy execution from the command line.



A key idea, taken from Modern Jass, is to compile contracts separately. The original source files never change in any way. It has flaws, mainly syntactic (for example, the contract code is written inside double quotes), but it guarantees the following two properties that the reliability introduces to this approach:



Contracts are immediately attached to classes after they are processed, and therefore their original presentation as inert data (for example, string literals), passes through many forms throughout life. The following sections describe how contracts are translated from their specifications to actual bytecode. Section 4 describes the general compilation technique borrowed from AOP, while Section 5 describes the internal implementation in Cofoja.



4 Compiling the contractual aspect



Verification of contracts is created by cross-cutting in the code (crosscutting), if described by aspect-oriented terms. Although the contracts themselves determine the properties of the business logic of the program, their verification can be represented as Aspects of the application.



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



Cofoja 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 with the compilation of the Council code lies in such a 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 within the same boundaries as the code being changed. The precondition, for example, probably checks the arguments of the call, or any contract may want to call a private class method. This is easy to achieve if the compiler knows this; The 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 a copy of the original class, turning into bytecode, and as a result, the resulting compiled methods are extracted. These methods can easily be linked into the final classes (as additional methods) before they load. Thus, the bytecode belongs to an additional aspect, besides compiled and saved separately and fully reusable.



The technique has improved, so that the methods of the original class can be replaced by plugs. What is important is that the compiler properly generates calls to these methods within the Council Code; and their actual content does not matter. In this regard, the standard annotation processing API provides sufficient information to easily formed stubs by the reflected members of the class hierarchy. An additional benefit is the extensions of the applicability of classes available only as bytecode: method signatures can be read from class files, ignoring the associated method bodies.



4.2 Connection points and linking


Binding ends through byte-code rewriting: additional methods are added to the class and methods, to which the tips are applied, 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, the parts of the Board that surround the method and have post-conditions with old-value expressions are commonplace, but special cases for which context must be kept. In Cofoja, the decision to save the context is made by setting additional local variables that are added to the post-execution signature of the Council method.



Contracts are particularly suitable for this approach, because the context of information is naturally divided into a set of non-overlapping variables. Two alternatives: embedding inside the Council's bytecode methods and splitting the Council-method inside the auxiliary entity.



Embedding methods into the 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 down the benefits of access boundaries.



A more general strategy is to position 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 is subordinate to the Council methods that are responsible for calling the auxiliary procedure .



4.3 Board 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 the Council-methods are naturally inherited through the normal class hierarchy and they are available at the time of binding. With some extra effort, they can also be available with source code.



Depending on the application, the inherited Council can greatly change its very 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 the writing of the Council for the interface is an important component if there is a way to connect these pieces into specific classes that implement this interface. Obviously, the path of injecting the Aspect code into the original interface is impossible; the resulting java file will not even compile and it hits on the design 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 solution is to use the existing connected infrastructure: classes that implement the interface can easily attach methods-tips and continue their existence as usual. However, care should be taken when converting all references to the implemented class to references of the actual class whose methods are injected. There are also tasks with code duplication.



The second solution requires that the interface pieces for the interface be reworked to work with an additional parameter that is valid to control the actual object. However, this eliminates any duplication. It should be noted that the hope for external procedures does not limit the expressiveness of these structures, since interfaces have only public constructs.



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, who applies the second solution.



4.4 Limitations of the Compilation Technique


This Aspect compilation approach is guaranteed that the Java compiler does not optimize the method within its boundaries. In fact, this requires that source methods and bytecode methods be combined one-to-one, for example, there is no fragmentation of the method when compiling. If there are stubs, embedding directly a piece of the method is another big undesirable optimization. In practice, this is not a big problem, given the current trend towards optimizing the level of the virtual machine than the compiler. In addition, the Contracts, in particular, are intended mainly for the development and debugging purposes, and therefore, probably, will not be compiled with optimization included.



Another possible more serious problem is compilation errors. Error reporting requires more caution, because he tends to give out elusive contradictions. A simple idea is to give the result from the main compiler process, so that the user is shown formed messages not related to the user's code, but corresponding to the mixed code with the generated elements. Cofoja complements this option with advanced features to help clarify common error messages; a more general solution would use improved integration with the compiler API.



List of references


Source: https://habr.com/ru/post/139206/

More articles:



All Articles