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 Jahob.
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)); } } }
Examples of Functions with Specifications
For homework, you will have more such examples.