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

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

A verification condition formula for preserving an invariant:

  • we will see methods to prove such invariants

Transforming iterative version

  • changing initial condition

Summary of these Small Examples

Some other Examples done in Jahob

Another System

 
sav08/proving_correctness_of_some_small_examples.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice