## ← Automated Inferring Solution - Software Debugging

• 3 Followers
• 18 Lines

### Get Embed Code x Embed video Use the following code to embed this video. See our usage guide for more details on embedding. Paste this in your document somewhere (closest to the closing body tag is preferable): ```<script type="text/javascript" src='https://amara.org/embedder-iframe'></script> ``` Paste this inside your HTML body, where you want to include the widget: ```<div class="amara-embed" data-url="http://www.youtube.com/watch?v=grQfebm_Ztw" data-team="udacity"></div> ``` 4 Languages

Showing Revision 3 created 05/25/2016 by Udacity Robot.

1. Thank you very much, and now for the answer.
2. The answer is if we want to have correct ranges for the input variables
3. as well as for the output variables,
4. we need to provide these ranges when calling square root.
5. In our case, the correct range for x is 0 to maxint.
6. If we invoke square root with 0, and if we invoke square root with the maximum integer,
7. what we're going to get is that x is greater or equal than 0
8. and x is less or equal than maxint,
9. which is actually the correct range.
10. Likewise, we've learned that the return value is always greater or equal than 0,
11. and it's always less or equal than the square root of maxint.
12. If we invoke the square root with a value of 1, this won't change a lot.
13. We will slightly expand the range, but we won't get the 0 in here.
14. This is actually not needed.
15. If we invoke square root with -1, then we will actually violate the implicit precondition.
16. Let's hope that square root then will actually fail
17. such that Daikon can then deduce that if we invoke square root
18. with a negative number it fails. These two are the correct values.