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

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?
• Proof of first lecture01 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?
• Notion of inductive loop invariant
• What is and is not inductive loop invariant in this example

A verification condition formula for preserving an invariant:

  r = i * x \land i=i+1 \land r' = r + x \rightarrow r' = i' * x

• we will see methods to prove such invariants

• changing initial condition

Examples of Functions with Specifications

• http://javaverification.org/

• VCC: A Verifier for Concurrent C