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

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

Examples of Functions with Specifications

For homework, you will have more such examples.