WEBVTT

00:00:00.000 --> 00:00:03.000
Let me show you how this works on an example.

00:00:03.000 --> 00:00:05.000
Here is a square root function.

00:00:05.000 --> 00:00:07.000
It takes x and returns the square root.

00:00:07.000 --> 00:00:10.000
Let's assume we invoke this with the values 2, 4, and 16.

00:00:10.000 --> 00:00:13.000
When we invoke the square root with the value of 2,

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.

00:00:19.000 --> 00:00:22.000
However, these patterns would also be instantiated:

00:00:22.000 --> 00:00:27.000
x is smaller or equal than two, and x is greater or equal than 2,

00:00:27.000 --> 00:00:30.000
because these patterns also hold for the values that we observed.

00:00:30.000 --> 00:00:33.000
In the next iteration, we invoke the square root with the number of four,

00:00:33.000 --> 00:00:37.000
and now, the invariant of x always being 2 is eliminated.

00:00:37.000 --> 00:00:42.000
What we get now, however, is that x being less or equal than 4 still holds.

00:00:42.000 --> 00:00:45.000
We can do so by merging the earlier invariant with a new one.

00:00:45.000 --> 00:00:50.000
And x greater or equal than 2 still holds for the new value.

00:00:50.000 --> 00:00:54.000
When we invoke the square root of 16, we now retain the invariant

00:00:54.000 --> 00:00:58.584
that x is less or equal than 16 and greater or equal than 2,

00:00:58.584 --> 00:01:00.000
and this is what we get in the end:

00:01:00.000 --> 00:01:05.000
x is between 2 and 16, and eps is always 10^-7.

00:01:05.000 --> 00:01:09.000
For the postcondition, we get similar ranges for the return value.

00:01:09.000 --> 00:01:12.000
The return value is between the square root of 2 and 4,

00:01:12.000 --> 00:01:14.000
which is the square root of 16.

00:01:14.000 --> 00:01:20.000
However, what we also get is that the return value squared is equal to x,

00:01:20.000 --> 00:01:24.000
and we get this because Daikon has an appropriate pattern for that,

00:01:24.000 --> 00:01:31.000
namely a pattern where the multiplication of any two variables equals a third variable,

00:01:31.000 --> 00:01:36.000
and this is instantiated with a return value, again with a return value and with x

00:01:36.000 --> 00:01:39.000
and this pattern then holds for all runs--

00:01:39.000 --> 00:01:41.000
at least for all runs with integer numbers.

00:01:41.000 --> 00:01:45.000
If we put in floating point numbers, then eps also comes into play,

00:01:45.000 --> 00:01:49.000
because of rounding errors, and then this pattern would no longer be discovered.

00:01:49.000 --> 00:01:53.000
So whatever Daikon can produce is constrained to the pattern library it has,

00:01:53.000 --> 00:01:57.000
but if you add more patterns, then you'll be able to discover more properties,

00:01:57.000 --> 00:02:00.000
which will take Daikon a bit longer, though, to discover them.

00:02:00.000 --> 00:02:03.000
Still, even with a perfect set of patterns,

00:02:03.000 --> 00:02:06.000
approaches like these are dependent on the actual numbers

00:02:06.000 --> 00:02:08.000
that are being fed in there.

00:02:08.000 --> 00:02:11.000
What Daikon produces is relevant for all the runs observed,

00:02:11.000 --> 00:02:14.000
but we all know that the real precondition for the square root

00:02:14.000 --> 00:02:17.000
does not have specific range constraints on x

00:02:17.000 --> 00:02:19.000
except that x should be greater or equal than 0.

00:02:19.000 --> 00:02:24.000
Likewise, the return value of square root is not necessarily between the square root of 2

00:02:24.000 --> 00:02:26.000
and the square root of 16,

00:02:26.000 --> 00:02:29.000
but it can actually be anything that's, again, greater than 0.

00:02:29.000 --> 00:02:35.000
So, tools for dynamic inference of invariants can work well

00:02:35.000 --> 00:02:38.000
if they do have a good test suite in the beginning.

00:02:38.000 --> 00:02:42.000
How can we get the correct ranges for x and the return value?

00:02:42.000 --> 00:02:45.000
By invoking square root with a value of 0?

00:02:45.000 --> 00:02:49.000
By invoking square root with a value of 1?

00:02:49.000 --> 00:02:56.000
By invoking square root with a value of maxint, where maxint is the highest available integer?

00:02:56.000 --> 00:02:59.000
Or by invoking square root with a negative value?

00:02:59.000 --> 00:03:01.000
Hint: you need multiple invocations.

00:03:01.000 --> 00:03:04.304
Check those which you need to get the correct ranges. Over to you.