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:


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.
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.
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?
$n-j+1$ should work as it satisfied the three properties of a bound function.


It is definitely an integer valued function as all variables and 1 are integers.
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.
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 &lt; j$, since both $n$ and $j$ are integers. Since $j&gt;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&gt;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.