- English only

# Lab for Automated Reasoning and Analysis LARA

# Proving Correctness of Some Small Examples

In this demo we go through several examples and prove them correct using the Jahob system.

### A Recursive Function

Consider the following recursive function:

private static int f(int x, int y) { if (y == 0) { return 0; } else { if (y % 2 == 0) { int z = f(x, y / 2); return (2 * z); } else { return (x + f(x, y - 1)); } } }

- What does 'f' compute?
- How can we prove it?

#### An Iterative Example

private static int fi(int x, int y) { int r = 0; int i = 0; while (i < y) { i = i + 1; r = r + x; } return r; }

- How can we prove it?
- What is and is not inductive loop invariant in this example

A verification condition formula for preserving an invariant:

- we will see methods to prove such invariants

#### Transforming iterative version

- changing initial condition