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)); } } }
- What does 'f' compute?
- How can we prove it?
=== 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; }
- How can we prove it?
- What is and is not inductive loop invariant in this example
Transforming iterative version
Summary
Examples of Functions with Specifications
As part of homework, you will have another such example.