# 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. ðŸ‘»

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 Arrow 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 obey 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, Arrow 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, Arrow 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``

## Loopsâ€‹

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.