Problem $3(18$ pts$.)$: Loopy square root

Below we give, in Dafny syntax, the square root method which should be computing the square root of a number.a$)$ Test this code by creating the Main$()$ method and calling loopysqrt$()$ with arguments like $4,25,30,$ etc. to convince yourself that this algorithm appears to be working correctly. In your answer, describe your tests and the corresponding output. $(2$ pts$.)$b$)$ Yet, the code given above fails to verify with Dafny. One of the reasons for this is that it is actually incorrect. More specifically, this code may produce the result which does not comply with the specification. Write a test $($or tests$)$ that reveals the bug. In your answer, describe your test$($s$),$ the corresponding outputs, and the bug that you found. Also, indicate which part of the specification is violated. $(2$ pts$.)$c$)$ Now, make this code correct by changing the precondition. In your answer, describe the change and show the output of the re$-$run of the same tests you ran before. $(2$ pts$.)$d$)$ Does your Dafny code verify now? Why or why not? If it doesn't verify, does it mean that your code still has bugs in it$?(2$ pts$.)$e$)$ If your Dafny code doesn't verify, uncomment invariant and$/$or decreases annotations and supply the actual invariant and$/$or decrementing function. Make sure your code now verifies. In your answer, describe how you guessed the invariant and$/$or the decrementing function. Explain why your code was failing Dafny verification earlier but does verify now, despite the fact that you have not made any changes to your actual code $($annotations are not part of the code$).(2$ pts$.)$f$)$ Submit your final Dafny code. $(2$ pts$.,$ autograded$)$g$)$ Use computational induction to prove by hand the total correctness of the final version of your Dafny code. $(6$ pts$.)$