Minor nitpick: Around 2:35 the argument is made that one needs to ensure a minimum decrease for the loop termination expression; however this is not the case. Rather, it is sufficient and necessary that the sequence of values either diverges, or converges
to a value less than zero. For instance, both these loops will provably terminate, for any positive values of x and n:

/* decreases x - 1 */
while (x > 1)
{
x = x / 2;
}

/* decreases x */
while (x > 0)
{
x = x - (1 / n);
n = n + 1;
}

## Comments

## The Verification Corner - Loop Termination

Minor nitpick: Around 2:35 the argument is made that one needs to ensure a minimum decrease for the loop termination expression; however this is not the case. Rather, it is sufficient and necessary that the sequence of values either diverges, or converges to a value less than zero. For instance, both these loops will provably terminate, for any positive values of x and n: