Analysis

Arrow Analysis introduces new checks in your compilation pipeline, which warn about common mistakes like out of bounds indexing

Quickstart

This Quickstart explains how to set up Arrow Analysis in your Gradle project, and how to use it to get further insight in your code, and to introduce additional checks in your own functions and classes.

Pre and post-conditions

In Quickstart we've introduced the idea of pre and post-conditions of functions as promises that either the caller or the body of the function should obey. Here we go deeper in the topic, about how these conditions may look, how they compose, and which way they are checked.

Control operators

When dealing with pre-conditions, the environment in which a call takes place is very important. You introduce new information in the environment every time you use a control operator like if or when. For example, the following is accepted by Arrow Analysis, when you manually checking whether the size of the list is enough for getin the right value:

Mutability and loops

Arrow Analysis supports mutability at the level of functions (but not yet at the level of classes). However, when you declare something with var, things get tricky. 👻

Types and invariants

Classes and interfaces (which we shall collectively refer to as "types") play a crucial role in organizing data in Kotlin. Arrow Analysis builds upon this idea, giving users the ability to attach Boolean expressions related to the data contained in a class. We call those invariants of the type, since the tool enforces those expressions to be true throughout the whole program.

Fields and wrappers

Arrow Analysis supports the addition of invariants to types, but what happens when you already have a type and want to add information relative to it? And when may that situation arise? There are two different features to keep more information: fields and wrapper types.

3rd-party libraries (Laws)

Is a library you use not compiled with Arrow Analysis? I could tell you to open an issue in their repository and convince their authors, but this is not always possible. For those cases Arrow Analysis provides a way to declare pre- and postconditions separately from the implementation, using @Law annotations. In fact, this is the way we package the analysis information related to Kotlin's stdlib.

Java support

This is still an alpha feature.

GitHub Actions / SARIF

This is still an alpha feature.