deskin

deskin deskin

Niner since 2010

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:

     

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

     

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