Main website: https://www.e2immu.org.

1. Introduction

This document is work in progress. In some places, it is nothing but a skeleton.

2. Installing e2immu

2.1. Obtaining the analyser

For now, the analyser’s binaries have not been uploaded to a central jar repository (like MavenCentral) yet. Please clone the following projects from GitHub:

  • e2immu-support, a small jar containing the annotations and some support classes

  • e2immu, the analyser

The support jar has been compiled with the Java 10+ API; this can easily be stripped down to Java 8 if required. The analyser makes extensive use of the Java 16 API and language features.

The IntelliJ plugin is still in its infancy. It is not yet available in IntelliJ’s plugin repository. To experiment with it, clone

2.2. The support jar

The annotations and support classes can be compiled with any JDK providing the Java 10+ API. Execute:

./gradlew publishToMavenLocal

to make the jar, with reference org.e2immu:e2immu-support:0.2.0, locally available.

2.3. The analyser

Please ensure you have at least a Java 16 JDK. Gradle 7.0 (lower versions do not play nice with Java 16) is provided via the Gradle wrapper.

To make the jars available, publish them to your local Maven repository:

./gradlew publishToMavenLocal

This pushes the following jars to your local Maven repository:

  • org.e2immu:analyser:0.1.2, the analyser

  • org.e2immu:analyser-cli:0.1.2, a small library extending the analyser with a command line

  • org.e2immu:analyser-store-uploader:0.1.2, a small library to upload annotations to the annotation store

  • org.e2immu:gradle-plugin:0.1.2, the Gradle plugin which you’ll need to run the analyser in a practical setting

Of course, version numbers may have changed when you read this.

2.4. The annotation store

The annotation store is a separate project, consisting of two Java classes. Build it with:

./gradlew build

and start the annotation store with

./gradlew run

The build.gradle file provides support to change the port, in case 8281 is already occupied. For example,

./gradlew run -De2immu-port=9999

will start the annotation store listening to port 9999. Please make sure this change of port is reflected in the configuration of the IDE plugin, which also needs to connect to the annotation store.

2.5. The IntelliJ plugin

The plugin is compiled with Java 8 language features only.

At this point (April 2021), the analyser still crashes on the sources of the plugin!

Using e2immu

3. Using e2immu

3.1. Basic use

Starting your first project, basic use of the e2immu analyser looks like

e2immu basic use
Figure 1. Basic use of e2immu

Having installed e2immu 's IntelliJ IDEA plugin, and having started a local annotation server, you can edit your project, occasionally run the analyser, and make use of pre-annotated libraries.

The analyser produces computed annotations, errors and warnings, which you can of course read from the command line. It also pushes these errors, warnings, and computed annotations to the annotation server, which is continuously consulted by the highlighter plugin. So while you’re working on your project, each time you run the analyser, your editor is updated. We’re suggesting that you confirm critical annotations in the source code. They will get the annotation type VERIFY which is the default for source code read by the analyser, they allow you to 'stabilize' your code with respect to class types like @Container or @E2Immutable .

This set-up will get you pretty far, as long as

  • your project consists of a single set of source files

  • all the libraries you are using have been pre-annotated.

3.2. Full flow

The e2immu analyser is set up to read, in order of decreasing priority,

  1. the source code of your project

  2. annotated API sources, as a replacement for class files with XML annotations

  3. class files and associated XML annotation files from jars, for libraries used in your project

If your project is or becomes a library for other projects to use, the computed annotations have to be made available to the users of the library:

  1. for fast turn-around development on your own or in small teams, you can use the analyser run on the library. This is depicted in Fast turnaround use of e2immu. to upload computed annotations to the annotation store, and instruct the analyser on the project consuming the library to consult this store. For this purpose, the annotation store has the ability to store annotations in user-defined projects; the analyser can read from any such projects.

  2. the standard procedure is for the computed annotations to be included in the jar file of the project: the analyser can directly write annotations.xml files in the resources of your project, one for each package. This action can take place after the compilation phase and before the packaging phase in you build tool. e2immu provides a plugin for Gradle for now. This flow is depicted in Add annotation.xml files to your jar.

e2immu fast turnaround
Figure 2. Fast turnaround use of e2immu
e2immu annotated xml via gradle
Figure 3. Add annotation.xml files to your jar

If you are annotating external libraries with e2immu annotations, there are two options

  1. you can use the external annotations feature of IntelliJ IDEA to create annotations files. These files are best grouped into a new jar file, on per library, which is to be included in the dependencies of your project.

  2. you can use annotated API sources, a kind of Java source file which contains all the declarative aspects of the types you’ll be using. These files are quick to create, provide a nice overview, and can be used in combination with the underlying JAR so that you only have to copy those declarations that you want to annotate. Their main advantage is clarity: all types, fields, and methods relevant to you are close together, with their annotations

Annotated API sources can be generated by the analyser from jars and XML annotations, presenting only those types, methods and fields that your project is using.

Updated annotation files can be generated by the analyser from the combination of annotated API sources and existing annotation files.

3.3. The analyser’s command line

The input to the analyser is largely controlled by the following primary locations

  • --source=<dir>: the directories where .java sources are to be found. They can be : or , separated; the argument can also be repeated. When nothing is specified, the analyser assumes src/main/java.

  • --classpath=<cp>: the classpath. This classpath should include the .class files corresponding to the .java files presented to the analyser. The format is as parsed by the JDK classpath: colon separated, with wildcards for multipe jar files in the same directory, containing jar files, .class files, or directories. Multiple --classpath options may be present; all are concatenated. When nothing is specified, build/classes/java/main:build/resources/main is assumed.

  • --jre=<dir>: location of the JRE if a different one from the analyser’s is to be taken

  • --restrict-source=<packages>: restrict the input to the following packages. The parameter can be comma separated, with wildcards as detailed in the note below.

The Maven or Gradle plugin typically takes care of correct values for source input and classpath.

Then there are typical options like

  • --quiet (short -q): do not write warnings, errors, etc to the standard output. They are still uploaded when the --upload option is activated.

  • --debug=<logtargets>: log targets to activate for debug output. Their names can be found in the class org.e2immu.analyser.util.Logger.LogTarget.

  • --ignore-errors: do not end the analyser in an error state when errors have been raised by the analyser.

The following options are available to control the output to the annotation server:

  • --upload (short: -u): upload annotations to an annotation server

  • --upload-url=<url>, change the default URL which is http://localhost:8281

  • --upload-project=<project>, change the default project which is default

  • --upload-packages=<packages>: a comma-separated list of package names for which annotations are to be uploaded. The default is to upload all annotations of all types encountered during the parsing process.

The following options are available to control the output of Annotation XML files written:

  • --write-annotation-xml (short: -w): create annotation files to be included in the resources, and hence the jar of the project.

  • --write-annotation-xml-packages=<packages>: a comma-separated list of package names for which annotation.xml files are to be written. The default is to write them for all the packages of .java files parsed

  • --write-annotation-xml-dir=<directory>: alternative location to write the Xml files. The value defaults to the resources directory of the project.

  • --write-annotated-api (short: -a)

  • --write-annotated-api-packages=<packages>: a comma-separated list of package names for which annotated API files are to be written. The default is to write them for all the packages of .java files parsed.

  • --write-annotated-api-dir=<directory>: alternative location to write the annotated API files. The default is the main directory of the project

When describing packages, a dot at the end of a package name may be used to indicate the inclusion of all sub-packages. The wildcard java. includes java.lang, java.io, etc.

3.4. The Gradle plugin

The easiest way to use the analyser is via the Gradle plugin.

Example of build.gradle file
plugins {
    id 'java'
    id 'org.e2immu.analyser'
}

...

repositories {
    ...
}

dependencies {
   ...
}

e2immu {
    skipProject = false
    sourcePackages = 'org.e2immu.'
    jmods = 'java.base.jmod,java.se.jmod'
    jre = '/Library/Java/JavaVirtualMachines/openjdk-11.0.2.jdk/Contents/Home/'
    writeAnnotatedAPIPackages = 'org.e2immu.'
    writeAnnotationXMLPackages = 'org.e2immu.'
}

The list of properties configurable differs slightly from the one of the command line. Gradle takes care of source and class path.

4. Annotated APIs

4.1. Purpose

The modification status of a class often depends on foreign method calls: calls on objects defined outside your own code base. In some situations, their source code is available, but that need not be the case. So to build up a fair picture, one could say that the e2immu analyser would have to parse all types and methods "from the ground up", and decide on their modification status in an incremental way. This procedure would be slow and hugely impractical.

On top of the incremental problem, APIs often come in the form of an interface without implementation. Expressing the modification status by hand (the terminology we use is contracting, or writing the contract) is the only way forward.

Thirdly, manually annotating APIs can help you override the implied modification status, or any other feature supported by the analyser. Here are two simple examples why that can come in handy:

interface List<E> extends Collection<E> {
    ...
    @Modified
    boolean add(@NotNull E e);
}

Here, we acknowledge that add modifies the list, but we prohibit passing null as an element. Secondly, we may decide to ignore modifications to the output stream System.out, by writing

class System {

    @IgnoreModifications
    @NotNull
    static final PrintStream out;

    @NotNull
    @IgnoreModifications
    static final PrintStream err;

    ...
}

so that we can still claim that the following method is not modifying:

@NotModified
static int square(int x) {
    int result = x*x;
    System.out.println("The square of "+x+" is "+result);
    return result;
}

It should be clear from these examples, and from the terminology used throughout the rest of the documentation, that we express the modification status, and other aspects of the code, by means of Java annotations.

In this section, we describe a practical way of annotating foreign APIs; we call it simply Annotated API files. The next section deals with a more compact form, annotation XML files, which are less readable but (maybe) simpler and faster to load.

4.2. Preparing Annotated API files

Should we then start to systematically annotate all the libraries that our project uses? That is one way of approaching the problem; however, because we have a source code analyser at hand, we can easily detect exactly which types, methods, and fields are used by our code. The analyser’s command line interpreter (CLI) provides options for generating a template Annotated API file for a whole library, for selected packages, or for exactly those types, methods and fields required.

The following Gradle task, taken from the e2immu/annotation-store project, contains the code to produce a single IoVertxCore.java file:

Part of build-api.gradle in e2immu/annotation-store
plugins {
    id 'java'
}

task runIoVertxAAPI(type: JavaExec) {
    group = "Execution"
    description = "Prepare an AnnotatedAPI file for io.vertx.core"

    classpath = sourceSets.main.runtimeClasspath
    main = 'org.e2immu.analyser.cli.Main'

    Set<File> reducedClassPath = sourceSets.main.runtimeClasspath.toList()
    reducedClassPath += sourceSets.test.runtimeClasspath
    reducedClassPath.removeIf({ f -> f.path.contains("build/classes")
        || f.path.contains("build/resources") })

    args('--classpath=' + reducedClassPath.join(":") + ":jmods/java.base.jmod",
            '-a',
            "--write-annotated-api-packages=io.vertx.core",
            "--source=none",
            "-d=CONFIGURATION,BYTECODE_INSPECTOR")
}

The task can be run with the command ./gradlew -b build-api.gradle runIoVertxAAPI.

4.3. The Annotated API file format

Annotated API files are standard Java files, they will be inspected by a standard Java parser, so all normal syntax rules need to be followed. They deviate in the following way:

  • The primary types become sub-types of a primary type named after the package.

  • To ensure that there is no clash with preloaded primary types, they have a dollar $ suffix.

  • A string constant, PACKAGE_NAME, specifies the package to which 'dollar types' are transferred.

  • All types become classes, all methods return a default value. Actually, none of the decorations to a type, method, or field matter, as long as the analyser can identify the structure uniquely.

This excerpt from the annotated API file for java.util used by the tests in the analyser, shows what this looks like:

Start of the JavaUtil.java annotated API file
public class JavaUtil {
    public static final String PACKAGE_NAME = "java.util";

    static class Enumeration$ {
        boolean hasMoreElements() { return false; }
        E nextElement() { return null; }
        Iterator<E> asIterator() { return null; }
    }

    static class Map$ {
        static class Entry {
            K getKey() { return null; }
            V getValue() { return null; }
    ...

Once all relevant types, methods and fields can be written, they can be annotated, as in:

A second part of the JavaUtil.java annotated API file
public class JavaUtil {
    public static final String PACKAGE_NAME = "java.util";

    ...

    @Container
    // this is not in line with the JDK, but we will block null keys!
    static class Collection$<E>  {

        boolean add$Postcondition(E e) { return contains(e); }
        @Modified
        boolean add(@Dependent1 @NotNull E e) { return true; }

        @Independent
        boolean addAll(@Dependent2 @NotNull1 java.util.Collection<? extends E> collection) {
            return true;
        }

        static boolean clear$Clear$Size(int i) { return i == 0; }
        @Modified
        void clear() { }

        static boolean contains$Value$Size(int i, Object o, boolean retVal) {
            return i != 0 && retVal;
        }
        @NotModified
        boolean contains(@NotNull Object object) { return true; }

        ...
    }
}

Also on display here are Companion methods, static methods describing either how the state of a Collection instance changes after a modifying method call, or certain edge cases can be resolved using this state information.

4.4. Annotation types

All e2immu annotations have a parameter of the enum type AnnotationType, which takes 4 different values:

VERIFY

this is the default value inserted when parsing Java code. This corresponds to the standard use of e2immu annotations: normally the analyser will compute them for you, but you may want to assert their presence.

VERIFY_ABSENT

mostly for debugging: insert in the Java code by hand to make sure the analyser does not end up computing this assertion for you.

COMPUTED

added to annotations inserted by the analyser

CONTRACT

added to annotations inserted when parsing annotation XMLs or annotated APIs. This type indicates that a value has not been computed, but stipulated by the user.

The list of available annotations can be found here. In Annotated API files, CONTRACT is the default type, and needs not be specified.

5. Annotation XML files

TODO

6. Visualising immutability

TODO

7. The annotation store as a demo project

This section assumes you have installed the analyser and its supporting jars, as described in Installing e2immu.

Next to playing a role in the communication between the IntelliJ plugin and the analyser, the annotation store serves as a demo project for the analyser. In its build.gradle file, the relevant lines to run the analyser are:

plugins {
    ...
    id 'org.e2immu.analyser'
}
...
e2immu {
    debug = "OUTPUT" //INSPECT,BYTECODE_INSPECTOR,ANALYSER,DELAYED"
    jmods = 'java.base.jmod,java.logging.jmod'
    sourcePackages = "org.e2immu.kvstore"
    readAnnotatedAPIPackages = "org.e2immu.kvstoreaapi"
    writeAnnotationXML = true
    writeAnnotationXMLPackages = "org.e2immu."
    upload = true
}

Because the analyser, as a Gradle plugin, is only available in your local Maven repository, the following lines need to be present in settings.gradle:

pluginManagement {
    repositories {
        mavenLocal()
        ...
    }
    resolutionStrategy {
        eachPlugin {
            if (requested.id.namespace == 'org.e2immu') {
                useModule('org.e2immu:gradle-plugin:0.1.2')
            }
        }
    }
}

Run the analyser:

./gradlew e2immu-analyser

It should "fail" with 2 errors and 4 warnings. If you have not started an annotation store (yet), you should also see an IOException warning you that uploading to the annotation store failed.

The debug options to e2immu listed above activate only the OUTPUT debug logger, which writes out the sources enriched with all annotations computed by the analyser. Run:

./gradlew e2immu-analyser --debug

to find them, obviously among a lot of other debug output.

Next to the build.gradle build file, there is a second one, build-api.gradle. It provides two tasks, runIoVertxInspected and runIoVertxUsage, which run the analyser via its command line interpreter rather than the Gradle plugin. Their primary goal is to produce templates for annotated API files. The former contains the option --write-annotated-api=INSPECTED, the latter the option --write-annotated-api=USAGE.

Executing:

./gradlew -b build-api.gradle runIoVertxUsage

runs the analyser without annotated API sources, which produces a lot of warnings, but also writes template files in the folder:

build/annotatedAPIs/org/e2immu/kvstoreaapi/

Reference

8. Concepts

8.1. Modification

8.2. Containers

8.3. Linking and independence

8.4. Immutability

8.4.1. Level 1 immutable

Terminology used:

Variable field

marked @Variable

Effectively final field

marked @E1Immutable or @E1Container .

Eventually final field

marked @E1Immutable or @E1Container , with after=xxx parameter

A type is level 1 immutable when all its fields are effectively final. A type is eventually level 1 immutable when after executing a marked method, the fields become effectively final. This transition is best understood as the removal of a number of methods, marked either @Mark or @Only with parameter before, which make the field variable.

8.4.2. Implicitly immutable types

Terminology:

Implicitly immutable content

all the fields of a type which are of implicitly immutable type.

8.4.3. Level 2 immutable

A type is level 2 immutable when

  1. it is level 1 immutable, i.e., all its fields are effectively final

  2. all fields are not modified

  3. if a field is not of implicitly immutable type, it must be either private, or level 2 immutable

  4. all constructors and non-private methods are independent of the fields

A type is eventually level 2 immutable when after executing a marked method, the fields become effectively final and or not modified. This transition is best understood as the removal of a number of methods, marked either @Mark or @Only with parameter before, which make the field variable or modify the fields.

8.4.4. Dynamic type annotations

8.5. Eventual immutability

8.6. Higher-order modifications

8.7. Miscellaneous

8.7.1. Constants

Java literals are constants. An instance of a type whose effectively final fields have only been assigned literal values, is a constant instance. Typical examples of a constant instances are found in parameterized enum fields.

8.7.2. Statement time

Technically important for variable fields (Level 1 immutable).

8.7.3. Singleton classes

8.7.4. Utility classes

A class which is at the same time eventually level 2 immutable, and cannot be instantiated.

The level 2 immutability ensures that the (static) fields are sufficiently immutable. The fact that it cannot be instantiated is verified by

  1. the fact that all constructors should be private;

  2. there should be at least one private constructor;

  3. no method or field can use the constructors to instantiate objects of this type.

8.7.5. Extension classes

An extension class is an eventually final type whose static methods all share the same type of first parameter.

8.7.6. Finalizers

9. Analyser details

9.1. Preconditions

TODO

9.2. Instance state

9.3. Companion methods

TODO

10. Overview of annotations

10.1. Annotation modes

Depending on where you find yourself in the continuum between object-oriented programming and functional programming, or, put differently, almost never following the container and level 2 immutable rules, or mostly adhering to them, you may wish to be either notified for following the rules, or warned by the analyser for breaking the rules. It is in this spirit that we envisage working in

Green mode

we assume that containers and level 2 immutable objects are sparse, and want to highlight when you follow the rules.

Red mode

when the majority of your types are level 2 immutable, and non-containers are rare, it may be more interesting to be warned when a type is not following the rules.

Because annotations often occur in an opposing pair, the choice of a mode can help to reduce information overload. For example, in red mode, @MutableModifiesArguments will be prominently displayed, and @E2Container will be "invisible". Similarly, @Modified is highlighted and @NotModified will be plain.

In green mode, we want @Container and @E2Container to be visible, while "normal" types are unmarked in black. The @NotModified will be highlighted, while @Modified remains plain.

10.2. Inheritance of annotations

In general, the analyser allows a method to do better than the method it overrides. It will raise an error when the overriding method is @Modified , where the original is @NotModified. TODO

10.3. List of annotations

For each of the annotations, we answer a couple of standard questions:

Basic

is this an annotation you definitely should understand?

Immu

is this annotation part of the immutability concept of the analyzer?

Contract

will you manually insert this annotation often in interfaces?

Type

does the annotation occur on types?

Field

does the annotation occur on (static) fields?

Method

does the annotation occur on methods and constructors?

Parameter

does the annotation occur on parameters?

This classification hopefully helps to see the wood for the trees in the long list.

10.3.1. @AllowsInterrupt

Basic

Immu

Contract

Type

Field

Method

Param

Contract-only annotation indicating that this method or constructor increases the statement time (Statement time), or allows the execution to be interrupted.

Default value is true. Methods can be annotated with @AllowsInterrupt(false) to explicitly mark that they do not interrupt.

External methods not annotated will not interrupt.

10.3.2. @BeforeMark

Basic

Immu

Contract

Type

Field

Method

Param

Summary

Annotation computed when an eventually immutable type is guaranteed to be in its before state, i.e., none of the marked methods have been called yet. As a dynamic type annotation (Dynamic type annotations), it is the opposite of @E1Immutable , @E2Immutable , or its container variants @E1Container , @E2Container . They guarantee that an eventually immutable object is in its after state, i.e., a marked method has been called, and the object has become immutable.

Mode

not immediately relevant

10.3.3. @Constant

Basic

Immu

Contract

Type

Field

Method

Param

Summary

The analyser emits this annotation when a field has a constant final value, or a method returns a constant value. Its primary purpose is to help debug the analyser. More details in Constants.

Mode

This annotation has no opposite.

Example

In this simple example, an enum constant is returned by the highest method:

@E2Container
public enum Enum_3 {
    ONE(1), TWO(2), THREE(3);

    public final int cnt;

    Enum_3(int cnt) {
        this.cnt = cnt;
    }

    @Constant("THREE")
    public static Enum_3 highest() {
        return THREE;
    }
}

10.3.4. @Container

Basic

Immu

Contract

Type

Field

Method

Param

Summary

The analyser computes this essential annotation for types which do not modify the parameters of their constructors and non-private methods. See Containers for an in-depth discussion.

Mode

Use this annotation in green mode. The opposite is @MutableModifiesArguments if the type has @Variable fields, or @E1Immutable if all the type’s fields are effectively final.

Example

The following examples present containers: @Constant, @Dependent, @E1Container. Non-containers are in @E1Immutable and @MutableModifiesArguments.

10.3.5. @Dependent

Basic

Immu

Contract

Type

Field

Method

Param

Summary

Annotation used to indicate that the type’s fields link to the method’s parameter or return value, or the constructor’s parameters. This annotation is only present for fields that are not of implicitly immutable type. Additionally, on methods, the analyser only computes the annotation when the method is @NotModified.

Mode

Use this annotation in the red mode. Its opposite is @Independent .

Example

The assignment of a mutable set to a field typically causes a dependency:

class Dependent<String> {
    private final Set<String> set;

    public Dependent(@Dependent Set<String> set) {
        this.set = set;
    }

    @Dependent
    public Set<String> getSet() {
        return set;
    }
}

A similar example is in @E1Immutable.

10.3.6. @Dependent1

Basic

Immu

Contract

Type

Field

Method

Param

Summary

As one of the Higher-order modifications annotations, @Dependent1 on a parameter, of implicitly immutable type, indicates that this parameter is assigned to one of the fields, or assigned into the object graph of one of the fields. When computed on a method, the return value of the method, again of implicitly immutable type, is known to be part of the object graph of the fields.

Mode

This annotation has no opposite. It implies @Independent because it appears on implicitly immutable types only.

Example

This annotation has been contracted in many collection-framework methods, such as

Collections.add(@Dependent1 E e);

@Dependent1
E List.get(int index);

The most direct example explaining the definition is:

public class Dependent1_0<T> {
    @Linked1(to = {"Dependent1_0:t"})
    private final T t;

    public Dependent1_0(@Dependent1 T t) {
        this.t = t;
    }

    @Dependent1
    public T getT() {
        return t;
    }
}

10.3.7. @Dependent2

Basic

Immu

Contract

Type

Field

Method

Param

Summary

This annotation is one of the Higher-order modifications annotations. It is only computed for independent parameters or methods. When computed on a parameter, it indicates that part of the implicitly immutable content of the argument will be assigned to the fields of the method’s type. When computed on a method, it signifies that part of the implicitly immutable content of the return value is assigned to the fields of the method’s type.

This annotation is central to iteration over the implicitly immutable content of a type.

Mode

This annotation has no opposite. By definition, implies @Independent .

Example

This annotation has been contracted in many collection-framework methods, such as

boolean Collections.addAll(@Dependent2 Collection<? extends E> coll);

@Dependent2
Stream<E> Collections.stream();

10.3.8. @E1Container

Basic

Immu

Contract

Type

Field

Method

Param

Summary

This annotation is a short-hand for the combination of @E1Immutable and @Container , as described in Level 1 immutable and Containers.

Mode

This annotation sits in between @MutableModifiesArguments , @Container and @E2Container .

Example

In the following example of an eventually level 1 immutable type, the field j remains variable until the user of the class calls setPositiveJ.

Example of an eventually @E1Container type
@E1Container(after = "j")
class EventuallyE1Immutable_2_M {

    @Modified
    private final Set<Integer> integers = new HashSet<>();

    @Final(after = "j")
    private int j;

    @Modified
    @Only(after = "j")
    public boolean addIfGreater(int i) {
        if (this.j <= 0) throw new UnsupportedOperationException("Not yet set");
        if (i >= this.j) {
            integers.add(i);
            return true;
        }
        return false;
    }

    @NotModified
    public Set<Integer> getIntegers() {
        return integers;
    }

    @NotModified
    public int getJ() {
        return j;
    }

    @Modified
    @Mark("j")
    public void setPositiveJ(int j) {
        if (j <= 0) throw new UnsupportedOperationException();
        if (this.j > 0) throw new UnsupportedOperationException("Already set");

        this.j = j;
    }

    @Modified
    @Only(before = "j")
    public void setNegativeJ(int j) {
        if (j > 0) throw new UnsupportedOperationException();
        if (this.j > 0) throw new UnsupportedOperationException("Already set");
        this.j = j;
    }
}

10.3.9. @E1Immutable

Basic

Immu

Contract

Type

Field

Method

Param

Summary

This annotation indicates that a type is level 1 immutable, effectively or eventually, meaning all fields are effectively or eventually final.

Mode

This annotation sits in between @MutableModifiesArguments and @E2Immutable .

Example

The add method modifies its parameter input; at the same time, the dependence between the constructor’s parameter and the field prevents the type from being level 2 immutable:

@E1Immutable
class AddToSet {
    private final Set<String> stringsToAdd;

    @Dependent
    public AddToSet(Set<String> set) {
        this.stringsToAdd = set;
    }

    public void add(@Modified @NotNull1 Set<String> input) {
        input.addAll(set);
    }
}

10.3.10. @E2Container

Basic

Immu

Contract

Type

Field

Method

Param

Summary

This annotation is a short-hand for the combination of @E2Immutable and @Container , as described in Level 2 immutable and Containers.

Mode

This annotation is the default in the red mode.

Example

TODO

10.3.11. @E2Immutable

Basic

Immu

Contract

Type

Field

Method

Param

Summary

This annotation indicates that a type is level 2 immutable, effectively or eventually.

Mode

This annotation is the default in the red mode.

Details

Level 2 immutability adds extra restrictions on top of level 1 immutability:

  1. all fields must be @NotModified;

  2. all fields must be either private, level 2 immutable, or of implicitly immutable type;

  3. all non-private methods and constructors must be marked @Independent

Example

TODO

10.3.12. @ExtensionClass

Basic

Immu

Contract

Type

Field

Method

Param

Summary

An extension class is a level 2 immutable class which uses More details can be found in Extension classes.

Example

TODO

10.3.13. @Final

Basic

Immu

Contract

Type

Field

Method

Param

Summary

This annotation indicates that a field is effectively or eventually final. Fields that have the Java modifier final possess the annotation, but the analyser does not write it out to avoid clutter.

Mode

Use this annotation to contract in the green mode, with the opposite, @Variable , being the default. In the red mode, @Final is the default.

Parameters

The after="mark" parameter indicates that the field is eventually final, after the marking method.

Details

A field is effectively final when no method, transitively reachable from a non-private non-constructor method, assigns to the field. A field is eventually final if the above definition holds when one excludes all the methods that are pre-marking, i.e., that hold an annotation @Only(before="mark") or @Mark("mark").

Example

Please find an example of an eventually final field in the example of @E1Container.

Example for @Variable, @Final
@Container
class ExampleManualVariableFinal {

    @Final
    private int i;

    @Variable
    private int j;

    public final int k; (1)

    public ExampleManualVariableFinal(int p, int q) {
        setI(p);
        this.k = q;
    }

    @NotModified
    public int getI() {
        return i;
    }

    @Modified (2)
    private void setI(int i) {
        this.i = i;
    }

    @NotModified
    public int getJ() {
        return j;
    }

    @Modified
    public void setJ(int j) {
        this.j = j;
    }
}
1 This field is effectively final, but there is no annotation because of the final modifier.
2 Note that only the constructor accesses this method.

10.3.14. @Finalizer

TODO

10.3.15. @Fluent

Basic

Immu

Contract

Type

Field

Method

Param

Summary

This annotation indicates that a method returns this, allowing for method chaining.

Mode

There is no opposite for this annotation.

Details

Fluent methods do not return a real value. This is of consequence in the definition of independence for methods, as dependence on this is ignored.

Example
@Fluent
public Builder setValue(char c) {
    this.c = c;
    return this;
}

10.3.16. @Identity

Basic

Immu

Contract

Type

Field

Method

Param

Summary

This annotation indicates that a method returns its first parameter.

Mode

There is no opposite for this annotation.

Details

Apart for all the obvious consequences, this annotation has an explicit effect on the linking of variables: a method marked @Identity only links to the first parameter.

Example
@Identity
public static <T> requireNonNull(T t) {
    if(t == null) throw new NullpointerException();
    return t;
}

10.3.17. @IgnoreModifications

Basic

Immu

Contract

Type

Field

Method

Param

Summary

Helper annotation to mark that modifications on a field are to be ignored, because they fall outside the scope of the application.

Mode

There is no opposite for this annotation. It can only be used for contracting, the analyser cannot generate it.

Example

The only current use is on System.out and System.err. The print method family is obviously modifying to these fields, however, we judge it to be outside the scope of the application.

10.3.18. @Independent

Basic

Immu

Contract

Type

Field

Method

Param

Summary

Annotation used to indicate that a method or constructor avoids linking the fields of the type to the return value and parameters. This annotation is only present when there are support data fields. Additionally, on methods, the analyser only computes the annotation when the method is @NotModified.

Mode

Use this annotation in the green mode. Its opposite is @Dependent .

  • TODO check definition for methods, parameters dependent as well?

  • TODO why do we ignore dependence on this?

10.3.19. @Linked

Basic

Immu

Contract

Type

Field

Method

Param

Summary

Annotation to help debug the dependence system.

Mode

There is no opposite.

10.3.20. @Linked1

TODO

10.3.21. @Mark

Basic

Immu

Contract

Type

Field

Method

Param

TODO

10.3.22. @Modified

Basic

Immu

Contract

Type

Field

Method

Param

Summary

Core annotation which indicates that modifications take place on a field, parameter, or in a method.

Mode

It is the default in the green mode, when @NotModified is not visible.

10.3.23. @Modified1

Basic

Immu

Contract

Type

Field

Method

Param

Summary

This annotation is part of the higher-order modifications.

Mode

the opposite annotation is @NotModified1. In green mode, this one is the default; in red mode, @NotModified1 is the default.

Example

Applying a c TODO

10.3.24. @MutableModifiesArguments

Basic

Immu

Contract

Type

Field

Method

Param

Summary

This annotation appears on types which are not a container and not level 1 immutable: at least one method will modify its parameters, and at least one field will be variable. Definitions are in Containers and Level 1 immutable.

Mode

It is the default in the green mode when none of @Container , @E1Immutable , @E1Container , @E2Immutable , @E2Container is present. Use it for contracting in the red mode.

Example

Types with non-private fields cannot be level 1 immutable. Here we combine that with a parameter modifying method:

@MutableModifiesArguments
class Mutate {
    @Variable
    public int count;

    public void add(@Modified List<String> list) {
        for(int i=0; i<count; i++) {
            list.add("item "+i);
        }
    }
}

10.3.25. @NotModified

Basic

Immu

Contract

Type

Field

Method

Param

Summary

Core annotation which indicates that no modifications take place on a field, parameter, or in a method.

Mode

It is the default in the red mode, when its opposite @Modified is not present.

Example

TODO

10.3.26. @NotModified1

Basic

Immu

Contract

Type

Field

Method

Param

Summary

This annotation is part of the higher-order modifications. Contracted to a parameter of an abstract type, it indicates that the abstract method cannot be implemented in a modifying way. Computed on parameters of any type with implicitly immutable content, it signifies that

Mode

It exists only in the green mode; there is no opposite. It can only be used for contracting, the analyser cannot generate it.

This annotation is a dynamic type annotation on functional types in fields, methods and parameters. The analyser can compute it in certain circumstances; in other cases, the user can show intent by requesting this property.

Note that because suppliers have no parameters, only modifications to the closure apply. Functional interfaces are always normally @NotModified: there are no modifying methods on them apart from the abstract method.

Example

We first show an example of a @NotModified1 contract:

Here, the analyser computes the annotation:

TODO

10.3.27. @NotNull

Basic

Immu

Contract

Type

Field

Method

Param

Summary

Core annotation to indicate that a field, parameter, or result of a method can never be null.

Mode

Use this annotation for contracting in the green mode. It is the opposite of @Nullable .

10.3.28. @NotNull1

Basic

Immu

Contract

Type

Field

Method

Param

10.3.29. @NotNull2

Basic

Immu

Contract

Type

Field

Method

Param

10.3.30. @Nullable

Basic

Immu

Contract

Type

Field

Method

Param

Summary

This annotation indicates that the field, parameter, or result of a method can be null.

Mode

This is the default in the green mode, when @NotNull is not present. Use it to contract in the red mode.

10.3.31. @Only

Basic

Immu

Contract

Type

Field

Method

Param

Summary

Essential annotation for methods in eventually immutable types.

Mode

There is no opposite.

Example

The following example shows a useful @Only(before="…​") method. Please find an example with a useful @Only(after="…​") method in @TestMark.

10.3.32. @PropagateModification

Basic

Immu

Contract

Type

Field

Method

Param

Summary

This annotation is part of the higher-order modifications. The analyser adds this annotation when an abstract method without modification information is called on a parameter. This abstract method can be modifying or not, and in general it cannot be known which is the case. The annotation then informs the analyser that modifications need computing at caller-time.

The annotation is also possible on fields, in case the parameter becomes the effectively final value of a field.

Mode

There is no opposite.

Example

A typical implementation of forEach is a nice example:

@FunctionalInterface
public interface Consumer<T> {
    void accept(T t); (1)
    ...
}
@Container
public interface Set<T> {
    default void forEach(@PropagateModification Consumer<T> consumer) {
      for(T t: this) consumer.accept(t);
    }
    ...
}
1 No modification information present on accept.

10.3.33. @Singleton

Basic

Immu

Contract

Type

Field

Method

Param

Summary

This annotation indicates that the class is a singleton: only one instance can exist.

Mode

There is no opposite for this annotation.

Example

There are many ways to ensure that a type has only one instance. This is the simplest example:

@Singleton
public class OnlyOne {
  public static final INSTANCE = new OnlyOne();

  public final int value;

  private OnlyOne() {
      value = new Random().nextInt(10);
  }
}

10.3.34. @TestMark

Basic

Immu

Contract

Type

Field

Method

Param

Summary

Part of the eventual system, this annotation is computed for methods which return the state of the object with respect to eventuality: after is true, while before is false.

Parameters

a parameter before exists to reverse the values: when before is true, the method returns true when the state is before and false when the state is after.

Mode

There is no opposite for this annotation.

Example

The @TestMark annotation in the following example returns true when t != null, i.e., after the marked method setT has been called:

@E2Immutable(after = "t")
public class EventuallyE2Immutable_2<T> {

    private T t;

    @Mark("t")
    public void setT(T t) {
        if (t == null) throw new NullPointerException();
        if (this.t != null) throw new UnsupportedOperationException();
        this.t = t;
    }

    @Only(after = "t")
    public T getT() {
        if (t == null) throw new UnsupportedOperationException();
        return t;
    }

    @TestMark("t")
    public boolean isSet() {
        return t != null;
    }
}

10.3.35. @UtilityClass

Basic

Immu

Contract

Type

Field

Method

Param

Summary

This annotation indicates that the type is a utility class: its static side is eventually level 2 immutable, and it cannot be instantiated. As a consequence, should only have static methods.

Mode

There is no opposite for this annotation.

Details

The level 2 immutability ensures that the (static) fields are sufficiently immutable. The fact that it cannot be instantiated is verified by

  1. the fact that all constructors should be private;

  2. there should be at least one private constructor;

  3. no method or field can use the constructors instantiate objects of this type.

Example

The following utility class is copied from the analyser:

@UtilityClass
public class IntUtil {

    private IntUtil() {
    }

    // copied from Guava, DoubleMath class
    public static boolean isMathematicalInteger(double x) {
        return !Double.isNaN(x) && !Double.isInfinite(x) && x == Math.rint(x);
    }
}

10.3.36. @Variable

Basic

Immu

Contract

Type

Field

Method

Param

Summary

This annotation indicates that a field is not effectively or eventually final, i.e., it is assigned to in methods accessible from non-private non-constructor methods in the type.

Mode

This annotation is the default in the green mode. It is the opposite of @Final .

Example

Any non-eventual type with setters will have fields marked @Variable :

@Container
class HoldsOneInteger {

  @Variable
  private int i;

  public void set(int i) {
    this.i = i;
  }

  public int get() {
    return i;
  }
}

10.4. Relations between annotations

In this section we summarize the relations between annotations.

10.4.1. On types

Note that:

  • @E2Container is a shorthand for the combination of @E2Immutable and @Container ;

  • @E1Container is a shorthand for the combination of @E1Immutable and @Container ;

  • @E2Immutable requires @E1Immutable ;

  • a type is @MutableModifiesArguments if and only if it is not @E1Immutable and not @Container ;

  • when a type is @MutableModifiesArguments , there will be at least one field marked @Variable , and at least one parameter marked @Modified ;

  • by definition, types without fields are @E2Immutable ;

  • all primitive types are implicitly @E2Container ; the analyser will not mark them.

10.4.2. On fields

Note that @Variable fields can be @NotNull ! This obviously requires a not-null initialiser to be present; all other assignments must be not-null as well. The opposite, a @Final field that is @Nullable , can only occur when the effectively final value is the null constant.

The following opposites are easily seen:

  • a field is either @Final or @Variable

  • a field is either @NotModified or @Modified

  • a field is either @NotNull (or @NotNull1 , or @NotNull2 ), or @Nullable (see also Nullability).

Note that:

  • @Variable implies @Modified , whether modifying methods exist for the field or not;

  • @Final @Modified : part of @E1Immutable ;

  • @Final @NotModified: part of @E2Immutable ; sufficient for implicitly immutable types; for other types, the visibility and dependence rules kick in.

From the field’s owning type, following the definitions, we obtain:

  • if a type is effectively @E2Immutable , all its fields are @Final @NotModified;

  • if a type is effectively @E1Immutable , all its fields are @Final ;

  • if a type is @MutableModifiesArguments , at least one of its field is @Variable .

Further, note that:

  • fields of a primitive type are always @NotNull and @NotModified, but neither are marked.

10.4.3. On constructors

Non-trivial constructors have the @Modified property. When there is support data, a constructor is either @Independent (green) or @Dependent (red). A constructor without annotations therefore implies either that the type is not @E1Immutable , or that the constructor is not assigning to support data fields.

10.4.4. On methods

Opposites:

  • a method is either @NotModified (green) or @Modified (red)

  • a method is either @Independent (green) or @Dependent (red). This property is only relevant when there is support data, and the method is @NotModified

  • a method is either @NotNull (or @NotNull1 , or @NotNull2 ) (green), or @Nullable (red)

Furthermore,

  • if a type is effectively @E2Immutable (green), all its methods are @NotModified (green).

Note that:

  • quite trivially, void methods have no annotations relating to a return element

  • methods returning a primitive type are @NotNull , but this is not marked

10.4.5. On parameters

Opposites:

  • a parameter is either @NotModified (green) or @Modified (red)

  • a parameter is either @NotNull (or @NotNull1 , or @NotNull2 ) (green), or @Nullable (red)

Implications:

  • if a type is @Container , the parameters of all non-private methods and constructors are @NotModified (green);

  • a parameter of primitive type, unbound parameter type, functional type, or @E2Immutable type, is always @NotModified (green);

Note that:

  • if a type is @MutableModifiesArguments (red), at least one of its parameters is @Modified (red), which will be marked;

  • quite trivially, parameters of a primitive type are always @NotNull and @NotModified, but we will not mark parameters of a primitive type.

10.4.6. Nullability

By convention,

  • @NotNull1 implies @NotNull

  • @NotNull2 implies @NotNull , @NotNull1

  • etc.

This way of working makes most sense in an immutable setting.

10.4.7. Eventually and effectively immutable

Field types and method return types can be eventually or effectively immutable when their formal type is not level 1 or level 2 immutable, but the dynamic or computed type is. In the latter case, static analysis shows that all assignments to the field, or all return statements, result in an immutable object. In the former case, object flow computation proves that the mark has been passed for this object to have become immutable.

When a type is level 1 or level 2 eventually immutable, and the object flow computation proves that all assignments or return statements yield an object which is in a state before the mark, the analyser will emit @BeforeMark .

Fields take the annotation of the eventual state, with the qualification of after="…​":

property not present eventually effectively

finality of field

@Variable

@Final(after="mark")

@Final

modification of field

@Modified

@NotModified(after="mark")

@NotModified

11. List of errors and warnings

11.1. Opinionated

The errors described in this section relate to bad practices that are not tolerated by the analyser:

ASSIGNMENT_TO_FIELD_OUTSIDE_TYPE

Assigning to a field outside the type of that field, is not allowed. Replace the assignment with a setter method. Try to do assignments as close as possible to object creation.

METHOD_SHOULD_BE_MARKED_STATIC

Methods which do not refer to the instance, should be marked static.

NON_PRIVATE_FIELD_NOT_FINAL

Non-private fields must be effectively final (marked @Final ). Who knows what can happen to the field if you allow that?

PARAMETER_SHOULD_NOT_BE_ASSIGNED_TO

Parameters should not be assigned to. The implementation of the analyser assumes that parameters cannot be assigned to, so this is probably the one error you really do not want to see.

11.2. Evaluation

ASSERT_EVALUATES_TO_CONSTANT_FALSE

The condition in the assert statement is always false.

ASSERT_EVALUATES_TO_CONSTANT_TRUE

The condition in the assert statement is always true.

CONDITION_EVALUATES_TO_CONSTANT_ENN

The null or not-null check in the if or switch statement evaluates to constant. This message is computed via a @NotNull on a field.

CONDITION_EVALUATES_TO_CONSTANT

The condition in the if or switch statement evaluates to a constant.

INLINE_CONDITION_EVALUATES_TO_CONSTANT

The condition in the inline conditional operator …​ ? …​ : …​ evaluates to a constant.

PART_OF_EXPRESSION_EVALUATES_TO_CONSTANT

Part of a short-circuit boolean expression (involving && or ||) evaluates to a constant.

11.3. Empty, unused

Errors of this type are typically trivial to clean up, so why not do it immediately?

EMPTY_LOOP

Empty loop: the loop will run over an Iterable which the analyser believes is empty.

IGNORING_RESULT_OF_METHOD_CALL

Ignoring result of method call. That’s fine when the method is modifying, but the call is pretty useless when the method is @NotModified.

UNNECESSARY_METHOD_CALL

Unnecessary method call, like, e.g., calling toString() on a String.

UNREACHABLE_STATEMENT

Unreachable statement, often because of an error from the Evaluation category.

UNUSED_LOCAL_VARIABLE

Unused local variable.

UNUSED_LOOP_VARIABLE

Unused loop variable.

UNUSED_PARAMETER

Unused parameter. Not raised when the method is overriding another method.

USELESS_ASSIGNMENT

Useless assignment.

TRIVIAL_CASES_IN_SWITCH

Trivial cases in switch.

PRIVATE_FIELD_NOT_READ

Private field not read outside constructors. If this is intentional, turn it into a local variable.

11.4. Verifying annotations

The following errors relate to the annotations you added to your source code, to verify that a type, method or field has a given property.

ANNOTATION_ABSENT

Annotation missing. You wrote the annotation in the source code, but it is absent from the computation of the analyser.

ANNOTATION_UNEXPECTEDLY_PRESENT

You explicitly write that the annotation should be absent, using absent=true, still, the analyser computes it.

CONTRADICTING_ANNOTATIONS

Contradicting annotations

WRONG_ANNOTATION_PARAMETER

Wrong annotation parameter: the annotation is both in the source code, and computed by the analyser. However, the associated values are differing.

WORSE_THAN_OVERRIDDEN_METHOD_PARAMETER

Property value worse than overridden method’s parameter

WORSE_THAN_OVERRIDDEN_METHOD

Property value worse than overridden method

11.5. Immutability

CALLING_MODIFYING_METHOD_ON_E2IMMU

Calling a modifying method on level 2 immutable type is not allowed. This error is typically raised when the type is only dynamically computed to be level 2 immutable, such as in the case of the immutable version of a collection.

DUPLICATE_MARK_CONDITION

Duplicate mark precondition

EVENTUAL_AFTER_REQUIRED

Calling a method requiring @Only(after) on an object in state @Only(before).

EVENTUAL_BEFORE_REQUIRED

Calling a method requiring @Only(before) on an object in state @Only(after).

INCOMPATIBLE_IMMUTABILITY_CONTRACT_AFTER_NOT_EE1

Incompatible immutability contract: Contracted to be @E2Immutable after the mark, formal type is not (eventually) @E1Immutable. Variants exist for @Only(before="…​"), and level 2 immutable.

INCOMPATIBLE_PRECONDITION

Incompatible preconditions

WRONG_PRECONDITION

Wrong precondition

PRECONDITION_ABSENT

Precondition missing

ONLY_WRONG_MARK_LABEL

@Only annotation, wrong mark label

MODIFICATION_NOT_ALLOWED

Illegal modification suspected

11.6. Odds and ends

CIRCULAR_TYPE_DEPENDENCY

Methods that call each other circularly, make it difficult for the analyser to compute modifications correctly.

DIVISION_BY_ZERO

The analyser suspects division by zero here.

FINALIZER_METHOD_CALLED_ON_FIELD_NOT_IN_FINALIZER

A @Finalizer method can only be called on a field, when in another @Finalizer method. Please refer to Finalizers.

FINALIZER_METHOD_CALLED_ON_PARAMETER=

A @Finalizer method cannot be called on a parameter. Please refer to Finalizers.

NULL_POINTER_EXCEPTION

The analyser suspects that this will always raise a null-pointer exception.

POTENTIAL_NULL_POINTER_EXCEPTION

The analyser suspects, and only warns, for a potential null-pointer exception.

TYPES_WITH_FINALIZER_ONLY_EFFECTIVELY_FINAL

Fields of types with a @Finalizer method can only be assigned to an effectively final ( @Final ) field. Please refer to Finalizers.

Technical

12. Supporting tools

12.1. Gradle plugin

The Gradle plugin greatly facilitates the use of the analyser by integrating it your project’s build process. We based its initial implementation on the one from SonarQube.

Example of build.gradle file
plugins {
    id 'java'
    id 'org.e2immu.analyser'
}

...

repositories {
    ...
}

dependencies {
   ...
}

e2immu {
    skipProject = false
    sourcePackages = 'org.e2immu.'
    jmods = 'java.base.jmod,java.se.jmod'
    jre = '/Library/Java/JavaVirtualMachines/openjdk-11.0.2.jdk/Contents/Home/'
    writeAnnotatedAPIPackages = 'org.e2immu.'
    writeAnnotationXMLPackages = 'org.e2immu.'
}

The list of properties configurable differs slightly from the one of the command line. Gradle takes care of source and class path.

12.2. Key-value store

The key-value store is a simple, two-class implementation of an independent key-value store acting as a bridge between the e2immu analyser and the IntelliJ IDEA plugin. It is mostly agnostic to the purpose in the project: it stores key-value pairs in sub-stores called projects.

Unless directed differently by the e2immu-port parameter, the store starts listening on port 8281 for HTTP communication. The protocol summary is:

# get an annotation name for an element
# curl http://localhost:8281/v1/get/project-name/element-description
#
# set the annotation name for an element
# curl http://localhost:8281/v1/set/project-name/element-description/annotation-name
#
# get annotation names for a whole list of elements
# curl -X POST @elements.json http://localhost:8281/v1/get/project-name
#
# set the annotation names for a whole map of elements
# curl -X PUT @elementsandannotations.json http://localhost:8281/v1/set/project-name
#
# get all key-value pairs for a project
# curl http://localhost:8281/v1/list/project-name
#
# list all projects
# curl http://localhost:8281/v1/list

Projects that do not exist will be created on-demand. The bulk get operation may receive more elements than that it asked for: depending on the effects of recent set operations, the store may include recently updated keys that were asked for recently as well.

Start the store by running:

~/g/e/annotation-store (master)> gradle run

> Task :annotation-store:run
Aug 01, 2020 9:19:55 AM org.e2immu.kvstore.Store
INFO: Started kv server on port 8281; read-within-millis 5000
<=========----> 75% EXECUTING [1m 39s]
> :annotation-store:run

In another terminal, experiment with the curl statements:

~> curl http://localhost:8281/v1/get/default/hello
{"hello":""}⏎
~> curl http://localhost:8281/v1/set/default/hello/there
{"updated":1,"ignored":0,"removed":0}⏎
~> curl http://localhost:8281/v1/get/default/hello
{"hello":"there"}⏎
~> curl http://localhost:8281/v1/set/default/its/me
{"updated":1,"ignored":0,"removed":0}⏎
~> curl http://localhost:8281/v1/list/default
{"its":"me","hello":"there"}⏎
~> curl http://localhost:8281/v1/list
{"projects":["default"]}⏎

Removing a key-value pair only works via the PUT method:

~> curl http://localhost:8281/v1/set/default/its/
<html><body><h1>Resource not found</h1></body></html>⏎
~> cat update.json
{"its":"","hello":"here"}
~> curl -X PUT -d @update.json  http://localhost:8281/v1/set/default
{"updated":1,"ignored":0,"removed":1}⏎
~> curl http://localhost:8281/v1/list/default
{"hello":"here"}⏎

12.3. IntelliJ IDEA plugin

Without a plugin for an IDE, the analyser would be hard to use, and the main purpose of the project, namely, unobtrusively assisting in better coding, would remain very far off. The current plugin for IntelliJ IDEA is absolutely minimal. We based our initial implementation on the Return statement highlighter plugin by Edoardo Luppi.

12.3.1. Visual objectives

For the proof of concept, we aim to color elements of the source code in such a way that there is visual information explaining why a type is not @E2Immutable or @Container . In the green mode, we highlight the immutable elements, which useful when they are sparse. In the red mode, we warn for mutable ones in an otherwise pretty immutable environment:

Following the Relations between annotations for types, we color:

annotation on type green mode red mode

@E2Container (incl. primitives)

green

black

@E2Immutable

green

black

@E1Container

brown

brown

@E1Immutable

brown

brown

@Container

blue

blue

@MutableModifiesArguments

black

red

@BeforeMark

purple

purple

For fields, we note that @Variable - @Final and @NotModified- @Modified can technically occur in each combination:

  • @Variable @Modified : impossible for unmodifiable types

  • @Variable @NotModified

  • @Final @Modified : part of @E1Immutable , impossible for unmodifiable types

  • @Final @NotModified: part of @E2Immutable

We therefore color the annotation hierarchy for fields as:

combination annotation on field green mode red mode

@Variable @Modified

@Variable

black

red

@Variable @NotModified

@Final @Modified

@Modified

brown

brown

@Final @NotModified, unmodifiable types

@Final

green

black

@Final @NotModified, modifiable types only

@NotModified

green

black

@SupportData (when field @NotModified and owning type @E1Immutable )

@SupportData

green italics

black italics

The @SupportData annotation is relevant to understand why a type is not level 2 immutable. In other situations, it simply clutters. The analyser will only emit it when the type is already @E1Immutable or @E1Container , and the field is already @NotModified.

The plugin transfers dynamic type annotations involving immutability (such as @E2Container ) from the field to the type. As a consequence, the left-hand side Set type will color green in:

private final Set<String> strings = Set.of("abc", "def");

according to the first color scheme.

Methods declarations mix dependency with modification. Independence is not necessary when there are no support types, and, given that we only start showing support data types when all fields are @NotModified, which implies that all methods are @NotModified, it makes sense to emit the dependency annotations only in the @NotModified situation:

annotation on method green mode red mode

@Independent (implying @NotModified)

green

black

@Dependent (implying @NotModified)

brown

brown

@NotModified (no support data)

green

black

@Modified

black

red

The interesting aspect to constructors is whether they are independent or not. To be consistent with the system for methods, the analyser will only emit the annotation when the type is showing support data.

annotation on constructor green mode red mode

@Independent (when support data)

green

black

@Dependent (when support data)

brown

brown

no support data

black

black

The situation of parameters is binary. The analyser colors:

annotation on parameter green mode red mode

@NotModified

green

black

@Modified

black

red

12.3.2. Information flow

Exactly which information does the analyser store in the key-value store? The keys are type names, method names, parameter names, or field names in a format that both analyser and plugin understand:

  • for a type, we use the fully qualified name, with sub-types separated by dots;

  • for a method, we use the distinguishing name, which is a slightly custom format that looks like

    type’s fully qualified name '.' method name '(' parameter type ',' parameter type …​ ')'

    where the parameter type is 'T#2' or 'M#0' when it is the third type parameter of the method’s type, or the first type parameter of the method, respectively. If the parameter type is not a type parameter, the fully qualified name suffices;

  • for a parameter, we append the '#' sign followed by the index to the method’s distinguishing name, starting from 0;

  • for a field, we use the fully qualified name of the type, a ':', and the name of the field.

On top of that comes the combination of a type and a field or method for the dynamic type annotations of fields and methods: the composite key is the field’s or method’s key followed by a space, and the type’s key.

The values consist of a single annotation type name in lowercase, like e2immutable or notmodified.

12.3.3. Implementation

The JavaAnnotator class links the plugin to the abstract syntax tree (or PSI in IntelliJ-speak). It is instrumental to decide which textual elements are to be highlighted.

The plugin framework creates the annotator on the basis of the java.xml configuration file. It is statically connected to the JavaConfig singleton instance which holds the configuration of the plugin.

It is also statically connected to the AnnotationStore singleton which is responsible for the assignment of elements to annotations. Elements will be described in a standardized format which will extend fully qualified type names. Annotations will be described as the simple names of the e2immu annotations.

The annotation store connects to an external server whose address is modifiable in the plugin configuration. By default, it connects to a local instance on http://localhost:8281. For now, this is a key-value store which keeps track of request and update times.

The annotation store keeps a cache where elements have a certain TTL. As soon as an element is not in the cache, the plugin requests the annotation value from the external server.

Where next?

There are many areas for improvement and extension:

  • much better information transfer between analyser, user, and source code

  • towards a full-option static code analyser

  • towards more automation for creating annotated API files

  • more plugins, for other build tools and other IDEs

  • …​

Copyright © 2020-2021, Bart Naudts, https://www.e2immu.org

This program is free software: you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. You should have received a copy of the GNU Lesser General Public License along with this program. If not, see http://www.gnu.org/licenses/.