[Script Info]
Title: 
[Events]
Format: Layer, Start, End, Style, Name, MarginL, MarginR, MarginV, Effect, Text
Dialogue: 0,0:00:00.00,0:00:03.00,Default,,0000,0000,0000,,Let me show you how this works on an example.
Dialogue: 0,0:00:03.00,0:00:05.00,Default,,0000,0000,0000,,Here is a square root function.
Dialogue: 0,0:00:05.00,0:00:07.00,Default,,0000,0000,0000,,It takes x and returns the square root.
Dialogue: 0,0:00:07.00,0:00:10.00,Default,,0000,0000,0000,,Let's assume we invoke this with the values 2, 4, and 16.
Dialogue: 0,0:00:10.00,0:00:13.00,Default,,0000,0000,0000,,When we invoke the square root with the value of 2,
Dialogue: 0,0:00:13.00,0:00:19.00,Default,,0000,0000,0000,,we could infer that x has a value of 2 and eps has a value of 10^-7.
Dialogue: 0,0:00:19.00,0:00:22.00,Default,,0000,0000,0000,,However, these patterns would also be instantiated:
Dialogue: 0,0:00:22.00,0:00:27.00,Default,,0000,0000,0000,,x is smaller or equal than two, and x is greater or equal than 2,
Dialogue: 0,0:00:27.00,0:00:30.00,Default,,0000,0000,0000,,because these patterns also hold for the values that we observed.
Dialogue: 0,0:00:30.00,0:00:33.00,Default,,0000,0000,0000,,In the next iteration, we invoke the square root with the number of four,
Dialogue: 0,0:00:33.00,0:00:37.00,Default,,0000,0000,0000,,and now, the invariant of x always being 2 is eliminated.
Dialogue: 0,0:00:37.00,0:00:42.00,Default,,0000,0000,0000,,What we get now, however, is that x being less or equal than 4 still holds.
Dialogue: 0,0:00:42.00,0:00:45.00,Default,,0000,0000,0000,,We can do so by merging the earlier invariant with a new one.
Dialogue: 0,0:00:45.00,0:00:50.00,Default,,0000,0000,0000,,And x greater or equal than 2 still holds for the new value.
Dialogue: 0,0:00:50.00,0:00:54.00,Default,,0000,0000,0000,,When we invoke the square root of 16, we now retain the invariant
Dialogue: 0,0:00:54.00,0:00:58.58,Default,,0000,0000,0000,,that x is less or equal than 16 and greater or equal than 2,
Dialogue: 0,0:00:58.58,0:01:00.00,Default,,0000,0000,0000,,and this is what we get in the end:
Dialogue: 0,0:01:00.00,0:01:05.00,Default,,0000,0000,0000,,x is between 2 and 16, and eps is always 10^-7.
Dialogue: 0,0:01:05.00,0:01:09.00,Default,,0000,0000,0000,,For the postcondition, we get similar ranges for the return value.
Dialogue: 0,0:01:09.00,0:01:12.00,Default,,0000,0000,0000,,The return value is between the square root of 2 and 4,
Dialogue: 0,0:01:12.00,0:01:14.00,Default,,0000,0000,0000,,which is the square root of 16.
Dialogue: 0,0:01:14.00,0:01:20.00,Default,,0000,0000,0000,,However, what we also get is that the return value squared is equal to x,
Dialogue: 0,0:01:20.00,0:01:24.00,Default,,0000,0000,0000,,and we get this because Daikon has an appropriate pattern for that,
Dialogue: 0,0:01:24.00,0:01:31.00,Default,,0000,0000,0000,,namely a pattern where the multiplication of any two variables equals a third variable,
Dialogue: 0,0:01:31.00,0:01:36.00,Default,,0000,0000,0000,,and this is instantiated with a return value, again with a return value and with x
Dialogue: 0,0:01:36.00,0:01:39.00,Default,,0000,0000,0000,,and this pattern then holds for all runs--
Dialogue: 0,0:01:39.00,0:01:41.00,Default,,0000,0000,0000,,at least for all runs with integer numbers.
Dialogue: 0,0:01:41.00,0:01:45.00,Default,,0000,0000,0000,,If we put in floating point numbers, then eps also comes into play,
Dialogue: 0,0:01:45.00,0:01:49.00,Default,,0000,0000,0000,,because of rounding errors, and then this pattern would no longer be discovered.
Dialogue: 0,0:01:49.00,0:01:53.00,Default,,0000,0000,0000,,So whatever Daikon can produce is constrained to the pattern library it has,
Dialogue: 0,0:01:53.00,0:01:57.00,Default,,0000,0000,0000,,but if you add more patterns, then you'll be able to discover more properties,
Dialogue: 0,0:01:57.00,0:02:00.00,Default,,0000,0000,0000,,which will take Daikon a bit longer, though, to discover them.
Dialogue: 0,0:02:00.00,0:02:03.00,Default,,0000,0000,0000,,Still, even with a perfect set of patterns,
Dialogue: 0,0:02:03.00,0:02:06.00,Default,,0000,0000,0000,,approaches like these are dependent on the actual numbers
Dialogue: 0,0:02:06.00,0:02:08.00,Default,,0000,0000,0000,,that are being fed in there.
Dialogue: 0,0:02:08.00,0:02:11.00,Default,,0000,0000,0000,,What Daikon produces is relevant for all the runs observed,
Dialogue: 0,0:02:11.00,0:02:14.00,Default,,0000,0000,0000,,but we all know that the real precondition for the square root
Dialogue: 0,0:02:14.00,0:02:17.00,Default,,0000,0000,0000,,does not have specific range constraints on x
Dialogue: 0,0:02:17.00,0:02:19.00,Default,,0000,0000,0000,,except that x should be greater or equal than 0.
Dialogue: 0,0:02:19.00,0:02:24.00,Default,,0000,0000,0000,,Likewise, the return value of square root is not necessarily between the square root of 2
Dialogue: 0,0:02:24.00,0:02:26.00,Default,,0000,0000,0000,,and the square root of 16,
Dialogue: 0,0:02:26.00,0:02:29.00,Default,,0000,0000,0000,,but it can actually be anything that's, again, greater than 0.
Dialogue: 0,0:02:29.00,0:02:35.00,Default,,0000,0000,0000,,So, tools for dynamic inference of invariants can work well
Dialogue: 0,0:02:35.00,0:02:38.00,Default,,0000,0000,0000,,if they do have a good test suite in the beginning.
Dialogue: 0,0:02:38.00,0:02:42.00,Default,,0000,0000,0000,,How can we get the correct ranges for x and the return value?
Dialogue: 0,0:02:42.00,0:02:45.00,Default,,0000,0000,0000,,By invoking square root with a value of 0?
Dialogue: 0,0:02:45.00,0:02:49.00,Default,,0000,0000,0000,,By invoking square root with a value of 1?
Dialogue: 0,0:02:49.00,0:02:56.00,Default,,0000,0000,0000,,By invoking square root with a value of maxint, where maxint is the highest available integer?
Dialogue: 0,0:02:56.00,0:02:59.00,Default,,0000,0000,0000,,Or by invoking square root with a negative value?
Dialogue: 0,0:02:59.00,0:03:01.00,Default,,0000,0000,0000,,Hint: you need multiple invocations.
Dialogue: 0,0:03:01.00,0:03:04.30,Default,,0000,0000,0000,,Check those which you need to get the correct ranges. Over to you.