LARA

This is an old revision of the document!


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));
    }
  }
}

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;
}

Transforming iterative version

  • changing initial condition

Summary of these Small Examples

Some other Examples done in Jahob

Another System