# Dealing with test condition '=' for a while loop when determining a bound function/loop variant

The following is the definition of what a bound function for a while loop must satisfy:

1. The bound function is an integer-valued, total function of some of the inputs, variables and global data that are defined when the loop is reached.

2. When the loop body is executed, the value of this function is decreased by at least one before the loop’s test is checked again, if at all.

3. If the value of this function is $$≤ 0$$ and the loop’s test is checked then the test fails (ending this execution of the loop).

I am given a while loop as such,

while (j ≤ n) {.....; j = j + 1}


where j is not touched by the rest of the body of the loop.

I am trying to find a bound function for this simple while loop. Here is what I tried:

• $$n-j$$ is not a bound function since point (3) fails.
• $$n-j-1$$ is not a bound function since the loop would not run initially if $$n=j$$ (since $$n-j-1=-1 \ge f(j,n)$$), and I am not sure if the latter is a total function due to the presence of $$-1$$.

How do I deal with the '=' in the '≤' to determine a bound function that satisfies the while loop?

• Are you just asking for for (long i = array.Length - 1; i >= 0; --i) { /* loop body */ }? That's a common idiom for moving backwards through an array. – Nat May 21 at 1:19
• no. Im asking for a bound function – SeesSound May 21 at 1:32
• What is $f(j,n)$ (originally $f(i,n)$)? – Yuval Filmus May 21 at 8:24

A bound function is $$n-j-1$$. Let us check the conditions one by one:
1. $$n-j-1$$ is an integer-value total function of some of the variables. (A function is total if it is defined on all inputs.)
2. When the loop body is executed, $$j$$ is increase by one, and so $$n-j-1$$ is decreased by one.
3. If $$n-j-1 \leq 0$$ then $$j \geq n-1$$ and so $$j > n$$, hence the loop condition "$$j \leq n$$" fails.
Another bound function is $$n-j-2$$: if $$n-j-2 \leq 0$$ then $$j > n+1$$ hence the loop condition fails.