# 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 '19 at 1:19
• no. Im asking for a bound function – SeesSound May 21 '19 at 1:32
• What is $f(j,n)$ (originally $f(i,n)$)? – Yuval Filmus May 21 '19 at 8:24

$$n-j+1$$ should work as it satisfied the three properties of a bound function.

1. It is definitely an integer valued function as all variables and 1 are integers.

2. Since $$j$$ is increased by 1 in every iteration, the function decreases by 1 each time. For example let's say $$n$$ was 5 and $$j$$ was 4. Then for the first iteration it would be 5-4+1=2, then the second iteration would be 5-5+1=1, and then when $$j$$ is 6, 5-6+1=0, which is also the upper bound for the number of executions of the loop body left.

3. Finally, if the value of the function is at most 0 then the test has to fail, and that is true for this function since if $$n-j+1\le0$$ then $$n+1\le j$$, which means that $$n < j$$, since both $$n$$ and $$j$$ are integers. Since $$j>n$$, that means the test must fail and that satisfies the final condition.

Thus $$n-j+1$$ is a bound function for this algorithm. The answer below is wrong: if $$n$$ was 5 and $$j$$ was 4 then $$n-j-1$$ would be 5-4-1=0 and so the function is at most 0, meaning that the test $$j\le n$$ must fail, but $$4\le 5$$ does not fail.

Furthermore, stating that $$n-j-1\le0$$ then $$j\ge n-1$$ implies $$j>n$$ is incorrect, as if $$j\ge n -1$$ how would $$j$$ be greater than $$n$$ for sure when it was just stated that $$j$$ could be greater than or equal to $$n-1$$? I am pointing out that the answer is wrong because I too had this same exact question and believed the answer provided before realizing it was incorrect, and so hopefully others would realize that too.

while (j <= n) is the same as while (j < n+1), and you know how to handle that, right?

So you find the correct solution for the first case, then replace n with n+1 everywhere. You could handle things like while (j+3 <= 2n-4) in exactly the same way, changing it to while (j < 2n-6), finding the solution for the first case, and replacing n with 2n-6.

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.

• j >= n-1 only implies j > n-2, not j > n. – gnasher729 Oct 1 '19 at 4:35