Contract programming in Java using the Google COFOJA library

What is used for

This technique provides verification of preconditions and postconditions when executing methods of classes, user-defined functions.

Like any other test, it allows you to increase the reliability of the program, ensuring the correctness of the data on the input and output. Or, lower (if used incorrectly).
')
Unlike assertions, checks are performed at runtime, i.e., directly during program execution and are present in the release version.

The essence of the method lies in the fact that with each subprogram, as it were, there is a “contract” to perform certain actions, i.e. It sets restrictions (conditions) on the range of input and output data. At the same time, the implementation of the "contract" (conditions) is tightly controlled.

Example

There is some class Time. Suppose it is very important, and the functioning of the entire universe depends on its work ...

The class has methods: getHours (), getMinutes (), getSeconds () and setHours (), setMinutes (), setSeconds (), respectively.

We describe it (part of the language constructs and mechanisms is omitted or simplified for brevity):

class Time { intHOURS; intMINUTES; intSECONDS; getHours(); { returnHOURS; } getMinutes(); { return MINUTES; } getSeconds() { return SECONDS; } setHours(newHOURS); { HOURS = newHOURS; } setMinutes(newMINUTES); { MINUTES = newMINUTES; } setSeconds(newSECONDS) { SECONDS = newSECONDS; } } * This source code was highlighted with Source Code Highlighter .

It is necessary to ensure that this class will return correct data, or it will not work at all (on the basis of the principle “Dead programs do not lie”).

How can I do that? Verification of data for correctness.

Path 1: Collective Farm

For the sake of brevity, we omit some details and repeating constructions of the class Time.

class Time { getHours(); { if (HOURS<0 ||HOURS>23) throw GREAT_Time_Exception ; return HOURS; } setHours(newHOURS); { if (newHOURS<0 ||newHOURS>23) throw GREAT_Time_Exception ; HOURS = newHOURS; } } * This source code was highlighted with Source Code Highlighter .

Disadvantages: Non-obviousness of verification. The need to write a bunch of code manually. Just now, we tried to apply a contract programming technique. But, this is PROVAAAAAAL! Why? We look further.

Path 2: Use a ready-made, elegant solution.

Java supports the annotation mechanism (recommendations to the compiler, preprocessor) - metadata that can be added to the program source code without affecting it semantically, i.e. without changing his behavior. At the same time, they can be used at the stage of code analysis, compilation and execution.

Than some employees of the Google company (David Morgan, Andreas Leitner, Nhat Minh Le - "Contracts for Java 20% Team") used. In their spare time, they developed the COFOJA annotation preprocessor library, which allows for implementing a contract-based programming methodology in Java.

Let's try using it for our Time class:

@Contracted // , – IDE class Time { @Ensures ({“result >= 0”,“result <= 23” }) getHours(); { return HOURS; } @Requires ({“newHOURS>= 0”,“newHOURS<= 23” }) @Ensures (“HOURS == newHOURS”) // // @Ensures (“getHours()== newHOURS”) setHours(newHOURS); { HOURS = newHOURS; } } * This source code was highlighted with Source Code Highlighter .

@Requires - literally means, “To make sure that BEFORE the subroutine is executed (“ condition is fulfilled ”)”. Otherwise, throw an exception.

@Ensures - literally means, “To make sure that AFTER a subroutine is executed (“ condition is fulfilled ”)”

Here we see that, as in Path1 , we check the preliminary and postconditions for our methods. What is the difference? The difference is that in the second case it is more obvious and convenient.

In addition to these two options, there are quite a large number of libraries and tools that allow using this technique in JAVA, but they are either outdated and not supported / not developed, or not so convenient to use.

What the library consists of.

com.google.java.contract. * is the main namespace of the COFOJA library.

It contains the implementation of the following annotations:

@Contracted - a hint for the IDE, says that the class uses contracts.

@Invariant - Invariants define the global properties of a certain class, which must be observed after its creation throughout its lifetime.

@Requires - defines preconditions - what should be true BEFORE entering a method or function.

@Ensures - defines postconditions - what should be true AFTER exiting a method or function.

@ThrowEnsures - allows you to generate a specified exception when performing postconditions.

What to look for.

@Ensures and @Requires each method can have only one. If you need to check several conditions, use the condition record in {}:

@Ensures ( { “1”, “ … ”, “N” } ) @Requires ( { “1”, “ … ”, “N” } ) * This source code was highlighted with Source Code Highlighter .

If the contract is not observed (violation of the necessary conditions), the library throws a PreconditionError exception - a precondition error that can be caught and processed.

Also, it is possible to generate your own exceptions when checking postconditions.
The annotation @ThrowEnsures is used for this. Its syntax is:

@ThrowEnsures ({ "" , "" }) @ThrowEnsures ({ "1" , "1" , ... "N" , "N" , }) * This source code was highlighted with Source Code Highlighter .

Contracts should not be used in order to check the data entered by the user for correctness - this is what the contracts were not intended for. They should only be used between software modules. Instead, implement validation of user input separately.

Configuring IDE for automatic work with contracts.

Eclipse *

Training:

We download / extract in any available way (up to compilation from source codes) package cofoja.jar .
We start IDE Eclipse , we create the new project.
Copy the file cofoja.jar to the root folder of the project.

Now we are going to configure the project:

Project -> Properties-> Java Build Path , Libraries tab -> Add JARs , in the appeared window select our file cofoja.jar
At this point, the Eclipse IDE will begin to recognize contract annotations. But that is not all. You need to tell the Eclipse IDE that when compiling our project, you need to use the EXTERNAL preprocessor of annotations.

To do this: go to the project menu Project -> Properties-> Java Compiler-> Annotation Processing , put all the checkboxes, add (key) two keys (Processor Options) :

com.google.java.contract.classpath - the absolute path to the file with the user annotation handler - cofoja.jar .
com.google.java.contract.classoutput is the absolute path to the folder into which all classes of the project are compiled ( bin folder).

Example :

com.google.java.contract.classpath = C: \ java \ eclipseWorkspace \ JavaContractsTest \ ccofoja.jar
com.google.java.contract.classoutput = C: \ java \ eclipseWorkspace \ JavaContractsTest \ bin

In the Factory Path subcategory, we tick the Enable Project Specific Settings checkbox, then - Add JARs -> select our cofoja.jar annotation processor .
After that, when compiling the project, the external annotation processor that we just configured should be used. But that is not all.
It remains to add one parameter of the virtual machine to run our code with the verification of contracts. To do this, in Run Configurations -> Arguments in the VM Arguments field specify: -javaagent: cofoja.jar
Format:
( -javaagent: <Contract_handle_file_name> .jar )
Is done. You can start writing code. After that, when compiling the project, errors in the annotations of contracts will be issued directly to the IDE .

NetBeans * **

1. Downloading / mining in any available way (up to compiling from source codes) package cofoja.jar .

2. Launch NetBeans IDE , create a new project.

3. Copy the file cofoja.jar to the root folder of the project.

4. Now proceed to the configuration of the project.

a. Project -> Properties-> Libraries

In the tabs Compile, Processor, Run add our file cofoja.jar (button Add JARs )

b. Go to Build -> Compiling

Check the boxes for Enable Annotation Processing, Enable Annotation Processing in Editor, then click on the Add button, and add the following line: com.google.java.contract.classpath

c. Go to the Run tab
Add the following to VM Options : -javaagent: cofoja.jar (the name of our contract-handler file)
Format:
( -javaagent: <Contract_handle_file_name> .jar )

d. Is done. You can start writing code. After that, when compiling the project, errors in the annotations of contracts will be issued directly to the IDE .

Javac - compile manually with annotations

1. Downloading / mining in any available way (up to compiling from source codes) package cofoja.jar .

2. Put the file cofoja.jar in one folder with the classes that we are going to compile, or specify the full path to it.

3. In the command line type: javac -cp cofoja.jar MyClass.java

Compile. Analyze error messages, if any, fix, re-compile.

The -cp compiler key allows you to specify annotation preprocessor. The following are the names of the files with the classes of your program.

The syntax is:
javac -cp <annotation_file_processor_name> <Class1.java> <ClassN.java>

* Note: If after the done actions you encounter an error message, which says that it is impossible to find a compiler ( JavaBuilder ), add the javac compiler directory (JDK \ bin) to the PATH system variable. After modifying this variable, it is necessary to reboot to make the changes take effect (for Windows 2k / XP, Windows 7 doesn’t need it. Linux may have to be re-logged depending on the shell used).

** Note: If there are no such menu items in your NetBeans , you may be using the old version. In NetBeans 6.9 , annotation support is definitely present — download and use it.