# Loop Invariants

To show how to verify loops, we will use a different example than our linked list for simplicity. We will write and verify a function that can add some value to every element of an array slice.

Let's write a function that takes an integer `x`

and sums up all values from 0 to that value in a loop.
For non-negative inputs, the result will be equal to `x * (x + 1) / 2`

:

```
// The next line is only required for doctests, you can ignore/remove it
extern crate prusti_contracts;
use prusti_contracts::*;
fn main() {}
#[requires(x >= 0)]
#[ensures(result == x * (x + 1) / 2)] //~ ERROR postcondition might not hold
fn summation(x: i32) -> i32 {
let mut i = 1;
let mut sum = 0;
while i <= x {
sum += i;
i += 1;
}
sum
}
// Prusti: fails
```

We cannot verify this code yet, because Prusti does not know what the `while`

loop does to `sum`

and `i`

. For that, we need to add a `body_invariant`

. Body invariants are expressions that always hold at the beginning and end of the loop body. In our case, the invariant is that `sum`

contains the sum of all values between 1 and `i`

. Since `i`

starts at 1 and not at 0, we have to slightly adjust the formula by using `i - 1`

instead of `i`

, so we get: `sum == (i - 1) * i / 2`

.

After adding the `body_invariant`

, we get this code:

```
// The next line is only required for doctests, you can ignore/remove it
extern crate prusti_contracts;
use prusti_contracts::*;
fn main() {}
#[requires(x >= 0)]
#[ensures(result == x * (x + 1) / 2)]
fn summation(x: i32) -> i32 {
let mut i = 1;
let mut sum = 0;
while i <= x {
body_invariant!(sum == (i - 1) * i / 2);
sum += i;
i += 1;
}
sum
}
// Prusti: verifies
```

This body invariant is enough to verify the postcondition. After the loop, `i == x + 1`

will hold. Plugging this into our `body_invariant!(sum == (i - 1) * i / 2)`

, we get `sum == x * (x + 1) / 2`

, which is our postcondition.

Note that we did not have to add `body_invariant!(1 <= i && i <= x)`

. In some cases, such as when the loop condition is side-effect free, Prusti adds the loop condition to the body invariant, as long as at least one `body_invariant`

is syntactically present in the loop.