Proving the correctness of a program

Question

So I have this program below SquareRootRecursion that I need to prove is correct. However i'm not sure what it's pre and post conditions would be and how I would use those to prove it's correctness.

SquareRoot(a)
   return SquareRootRecursion(a, 0, a+1)

SquareRootRecursion(a, b, c)
   if c = b + 1 then
      return b
   else
      d = (b + c) div 2
      if d^2 ≤ a then 
      return SquareRootRecursion(a, d, c)
      else 
         return SquareRootRecursion(a, b, d) 
      end if
   end if

Answer 1

Hint: Try working with small examples. We make the following claims:

• Throughout the recursion, the value of $a$ never changes.
• At the end of the recursion, we have that $b = \sqrt a$ and $c = \sqrt a + 1$.
• Throughout the recursion, we have that $b \leq \sqrt a < \sqrt a + 1 \leq c$.
• At each step in the recursion, either $b$ has increased by at least one or $c$ has decreased by at least one.