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

1. Title:
   Automated Inferring - Software Debugging
2. Description:

3. 0 0:00 - 0:03
   Let me show you how this works on an example.
4. 3000 0:03 - 0:05
   Here is a square root function.
5. 5000 0:05 - 0:07
   It takes x and returns the square root.
6. 7000 0:07 - 0:10
   Let's assume we invoke this with the values 2, 4, and 16.
7. 10000 0:10 - 0:13
   When we invoke the square root with the value of 2,
8. 13000 0:13 - 0:19
   we could infer that x has a value of 2 and eps has a value of 10^-7.
9. 19000 0:19 - 0:22
   However, these patterns would also be instantiated:
10. 22000 0:22 - 0:27
    x is smaller or equal than two, and x is greater or equal than 2,
11. 27000 0:27 - 0:30
    because these patterns also hold for the values that we observed.
12. 30000 0:30 - 0:33
    In the next iteration, we invoke the square root with the number of four,
13. 33000 0:33 - 0:37
    and now, the invariant of x always being 2 is eliminated.
14. 37000 0:37 - 0:42
    What we get now, however, is that x being less or equal than 4 still holds.
15. 42000 0:42 - 0:45
    We can do so by merging the earlier invariant with a new one.
16. 45000 0:45 - 0:50
    And x greater or equal than 2 still holds for the new value.
17. 50000 0:50 - 0:54
    When we invoke the square root of 16, we now retain the invariant
18. 54000 0:54 - 0:59
    that x is less or equal than 16 and greater or equal than 2,
19. 58584 0:59 - 1:00
    and this is what we get in the end:
20. 60000 1:00 - 1:05
    x is between 2 and 16, and eps is always 10^-7.
21. 65000 1:05 - 1:09
    For the postcondition, we get similar ranges for the return value.
22. 69000 1:09 - 1:12
    The return value is between the square root of 2 and 4,
23. 72000 1:12 - 1:14
    which is the square root of 16.
24. 74000 1:14 - 1:20
    However, what we also get is that the return value squared is equal to x,
25. 80000 1:20 - 1:24
    and we get this because Daikon has an appropriate pattern for that,
26. 84000 1:24 - 1:31
    namely a pattern where the multiplication of any two variables equals a third variable,
27. 91000 1:31 - 1:36
    and this is instantiated with a return value, again with a return value and with x
28. 96000 1:36 - 1:39
    and this pattern then holds for all runs--
29. 99000 1:39 - 1:41
    at least for all runs with integer numbers.
30. 101000 1:41 - 1:45
    If we put in floating point numbers, then eps also comes into play,
31. 105000 1:45 - 1:49
    because of rounding errors, and then this pattern would no longer be discovered.
32. 109000 1:49 - 1:53
    So whatever Daikon can produce is constrained to the pattern library it has,
33. 113000 1:53 - 1:57
    but if you add more patterns, then you'll be able to discover more properties,
34. 117000 1:57 - 2:00
    which will take Daikon a bit longer, though, to discover them.
35. 120000 2:00 - 2:03
    Still, even with a perfect set of patterns,
36. 123000 2:03 - 2:06
    approaches like these are dependent on the actual numbers
37. 126000 2:06 - 2:08
    that are being fed in there.
38. 128000 2:08 - 2:11
    What Daikon produces is relevant for all the runs observed,
39. 131000 2:11 - 2:14
    but we all know that the real precondition for the square root
40. 134000 2:14 - 2:17
    does not have specific range constraints on x
41. 137000 2:17 - 2:19
    except that x should be greater or equal than 0.
42. 139000 2:19 - 2:24
    Likewise, the return value of square root is not necessarily between the square root of 2
43. 144000 2:24 - 2:26
    and the square root of 16,
44. 146000 2:26 - 2:29
    but it can actually be anything that's, again, greater than 0.
45. 149000 2:29 - 2:35
    So, tools for dynamic inference of invariants can work well
46. 155000 2:35 - 2:38
    if they do have a good test suite in the beginning.
47. 158000 2:38 - 2:42
    How can we get the correct ranges for x and the return value?
48. 162000 2:42 - 2:45
    By invoking square root with a value of 0?
49. 165000 2:45 - 2:49
    By invoking square root with a value of 1?
50. 169000 2:49 - 2:56
    By invoking square root with a value of maxint, where maxint is the highest available integer?
51. 176000 2:56 - 2:59
    Or by invoking square root with a negative value?
52. 179000 2:59 - 3:01
    Hint: you need multiple invocations.
53. 181000 3:01 - 3:04
    Check those which you need to get the correct ranges. Over to you.