Let me show you how this works on an example.
Here is a square root function.
It takes x and returns the square root.
Let's assume we invoke this with the values 2, 4, and 16.
When we invoke the square root with the value of 2,
we could infer that x has a value of 2 and eps has a value of 10^-7.
However, these patterns would also be instantiated:
x is smaller or equal than two, and x is greater or equal than 2,
because these patterns also hold for the values that we observed.
In the next iteration, we invoke the square root with the number of four,
and now, the invariant of x always being 2 is eliminated.
What we get now, however, is that x being less or equal than 4 still holds.
We can do so by merging the earlier invariant with a new one.
And x greater or equal than 2 still holds for the new value.
When we invoke the square root of 16, we now retain the invariant
that x is less or equal than 16 and greater or equal than 2,
and this is what we get in the end:
x is between 2 and 16, and eps is always 10^-7.
For the postcondition, we get similar ranges for the return value.
The return value is between the square root of 2 and 4,
which is the square root of 16.
However, what we also get is that the return value squared is equal to x,
and we get this because Daikon has an appropriate pattern for that,
namely a pattern where the multiplication of any two variables equals a third variable,
and this is instantiated with a return value, again with a return value and with x
and this pattern then holds for all runs--
at least for all runs with integer numbers.
If we put in floating point numbers, then eps also comes into play,
because of rounding errors, and then this pattern would no longer be discovered.
So whatever Daikon can produce is constrained to the pattern library it has,
but if you add more patterns, then you'll be able to discover more properties,
which will take Daikon a bit longer, though, to discover them.
Still, even with a perfect set of patterns,
approaches like these are dependent on the actual numbers
that are being fed in there.
What Daikon produces is relevant for all the runs observed,
but we all know that the real precondition for the square root
does not have specific range constraints on x
except that x should be greater or equal than 0.
Likewise, the return value of square root is not necessarily between the square root of 2
and the square root of 16,
but it can actually be anything that's, again, greater than 0.
So, tools for dynamic inference of invariants can work well
if they do have a good test suite in the beginning.
How can we get the correct ranges for x and the return value?
By invoking square root with a value of 0?
By invoking square root with a value of 1?
By invoking square root with a value of maxint, where maxint is the highest available integer?
Or by invoking square root with a negative value?
Hint: you need multiple invocations.
Check those which you need to get the correct ranges. Over to you.