Comment by biot

Name and functionality inspired by Spec# [0] ... just a bit? Sample Spec# code:

  int ISqrt(int x)
    requires 0 <= x;
    ensures result*result <= x && x < (result+1)*(result+1);
  {
    int r = 0;
    while ((r+1)*(r+1) <= x)
      invariant r*r <= x;
    {
      r++;
    }
    return r;
  }

[0] http://research.microsoft.com/en-us/projects/specsharp/