Λrrow 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. 👻

When a local variable `x`

is immutable

```
val x = COMPLICATED_THING
```

the check knows upfront that any usage of `x`

correspond to the same `COMPLICATED_THING`

, wherever it’s used later on. However, if the declaration uses `var`

, at the point in which we use `x`

the value inside of it may be completely different from the first one!

The way out of this problem is to promise Λrrow Analysis that some condition over a mutable variable will *always* be true for the entire computation:

- the check can base its reasoning on this promise,
- but we need to check that you obbey your promise every time you try to give a new value.

We call this promise an **invariant** of the mutable variable.

As a consequence, if you do not declare an invariant, Λrrow Analysis knows nothing about your variable. Here’s an example which is “obviously” correct, but not accepted by the tool:

```
import arrow.analysis.post
fun usesMutability(x: Int): Int {
var z = 2
return z.post({ it > 0 }) { "greater than 0" }
}
```

```
e: declaration `usesMutability` fails to satisfy the post-condition: ($result > 0)
```

Let’s declare an invariant. We use the same syntax as post-conditions, but use the special function `invariant`

instead. Note that even though syntactically the invariant reads as part of the initial value, it really talks about the mutable variable being declared (`z`

in this case)
. After attaching this information to the variable, we are free to re-assign the variable, but we need to keep our promise.

```
import arrow.analysis.invariant
import arrow.analysis.post
fun usesMutability(x: Int): Int {
var z = 2.invariant({ it > 0 }) { "invariant it > 0" }
z = 3
return z.post({ it > 0 }) { "greater than 0" }
}
```

Of course, if we don’t keep our promise, Λrrow Analysis won’t be happy.

```
import arrow.analysis.invariant
import arrow.analysis.post
fun usesMutability(x: Int): Int {
var z = 2.invariant({ it > 0 }) { "invariant it > 0" }
z = 0 // 0 is not > 0
return z.post({ it > 0 }) { "greater than 0" }
}
```

```
e: invariants are not satisfied in `z = 0`
```

One place in which mutability is hard to avoid is loops. Our recommendation is to think carefully about invariants for your mutable variables, because a good choice will determine what can be checked. Here’s an example in which we compute the length of a list using a mutable integral variable:

```
import arrow.analysis.invariant
import arrow.analysis.post
fun <A> List<A>.count(): Int {
var count = 0.invariant({ it >= 0 }) { "z >= 0" }
for (elt in this) { count = count + 1 }
return count.post({ it >= 0 }) { "result >= 0" }
}
```

We are investigating ways to introduce additional information in the tool, like `for`

looping exactly many times as the `size`

of the list.

Do you like Arrow?

✖<