Exercise 7 from Microsoft's Dafny on Rise4Fun.com

dafny-exercise7

/*
 * Change the loop invariant to 0 <= i <= n+2. Does the loop still verify?
 * Does the assertion i == n after the loop still verify?
 * It no longer verifies because the invariant is no longer sufficient for
 * proving the assertion.
 */
method m(n: nat)
{
   var i: int := 0;
   while (i < n)
      invariant 0 <= i <= n+2;
   {
      i := i + 1;
   }
   assert i == n;
}