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