Dealing with test condition '=' for a while loop when determining a bound function/loop variant
$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.