Bounded Function

In mathematics, a function f defined on some set X with real or complex values is called bounded if the set of its values is bounded. In other words, there exists a real number M such that

$|f(x)|\le M$

SE212 Bounding Function

To show Total Correctness of a while-loop, we have to show the loop terminates.

To show termination, we identify a Bounding Function whose value:

1. is always greater than or equal to 0
2. decreases with every loop iteration
3. makes the loop’s guard become false as it approaches 0

Basically, just find an expression where if this expression is = 0, the program terminates.

assert(n > 0)
sum := 0;
j := 0;
while (j != n) do {
	sum := sum + a;
	j := j + 1;
};

In the example above, the bounding function is $n-j$, because it decreases as we loop more and more, and when $n-j==0$ the loop stops.

For Recursive functions, it’s very similar, except you have to use