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.
Ti mostro come funziona con un esempio.
Ecco una funzione square-root (radice quadra)
Prende x e ritorna la radice quadrata.
Supponiamo di chiamarla con i valori 2,4 e 16.
Quando chiamiamo square-root con valore 2,
possiamo dedurre che x abbia un valore 2 ed eps abbia un valore di 10 alla -7.
Comunque, questi pattern dovrebbero essere istanziati:
x e' <= di 2 e x >= di 2,
per far si' che questi pattern reggano anche per i valori che abbiamo osservato.
Nella successiva iterazione, chiamiamo square-root con il numero 4,
e ora, essendo l'invariante di x ancora 2, verra' eliminata.
Cio' che abbiamo adesso, comunque, e' che x <= 4 regge ancora.
Lo possiamo fare unendo l'invariante precedente con quella nuova,
e x >= 2 regge ancora con il nuovo valore.
Chiamando square-root(16), terremo ora l'invariante
per cui x <= 16 e >= 2,
e questo e' cio' che avremo alla fine:
x sara' tra 2 e 16 ed eps sempre 10 alla -7.
Come postcondizione avremo degli intervalli simili come valore di rientro.
Il valore di rientro e' tra radice quadra di 2 e 4,
che e' la radice quadra di 16.
Comunque, otteniamo pure che il valore di rientro a radice e' uguale a x
e lo otteniamo perche' Daikon ha un pattern apposito per questo,
ossia un pattern in cui la moltiplica di due variabili qualsiasi corrisponda ad una terza variabile
e cio' e' istanziato con un valore di rientro, di nuovo con un valore di rientro e con x
e questo pattern reggera' per tutte le esecuzioni --
almeno per tutte le esecuzioni con numeri interi.
Se ci mettiamo dentro numeri in virgola mobile, allora entra in gioco eps,
per via degli errori di arrotondamento e quindi questo pattern non verrebbe piu' considerato.
Quindi, qualunque cosa possa produrre Daikon e' ristretto alla sua libreria di pattern,
ma se tu ci aggiungi altri pattern sarai in grado di scoprire piu' proprieta',
a causa delle quali pero', Daikon diventera' piu' lento.
Eppure, anche con un set di pattern perfetto,
gli approcci come questo dipendono dai numeri che effettivamente
ci vengono messi dentro.
Cio' che produce Daikon e' rilevante per tutte le esecuzioni osservate,
ma sappiamo tutti che le precondizioni reali della radice quadrata
non sono ristrette ad uno specifico intervallo di x
a parte che x dev'essere >= 0.
Allo stesso modo, il valore ritornato da square-root non e' necessariamente tra la radice quadra di 2
e la radice quadra di 16,
ma potra' essere qualsiasi cosa che sia > 0.
Quindi, strumenti per la deduzione automatica delle invarianti puo' funzionare bene
se hanno una buona test suite iniziale.
Come possiamo ottentere gli intervalli giusti per x e i valori di rientro?
Chiamando square-root con valore 0?
Chiamando square-root con valore 1?
Chiamando square-root con valore di MAXINT, in cui MAXINT e' il piu' grande numero intero disponibile?
O chiamando square-root con un valore negativo?
Aiutino: ti servono piu' chiamate.
Segna quelle che ti servono ad ottenere i giusti intervalli. Tocca a te.
具体例を挙げて説明しましょう
平方根を求める関数において xを取得し平方根を返します
2､4､16という値で関数を呼び出します
平方根を2の値で呼び出すと
xは2でepsは10e-7の値であると推測できます
これらのパターンもインスタンス化します
xは2以上もしくはxは2以下である
これらのパターンは値には有効だからです
次の反復で平方根を4で呼び出します
するとxは常に2という不変条件が削除されます
しかしxは4以下であるという条件が有効になります
新たな値と以前の不変条件がマージするのです
xは2以上という条件は新しい値にも有効です
16の平方根を呼び出して 得られる不変条件は16以下かつ2以上で
これが最終的な条件です
xは2と16の間でepsは常に10e-7
事後条件に関しては戻り値の類似値域が分かります
戻り値は2と4の平方根の間です
これは16の平方根です
しかし2乗した戻り値は xと等しいということが分かります
Daikonが適切なパターンを有しているからです
つまり2つの変数の乗算は 3つ目の変数と等しいというパターンです
そして戻り値でインスタンス化され 再び戻り値とxでインスタンス化されます
このパターンは少なくとも 整数によるすべての実行で有効です
浮動小数点を入力すると 丸め誤差のためepsが始動します
そしてこのパターンはもう見つかりません
Daikonはパターンライブラリにあるものしか 作り出せませんが
パターンを追加すれば さらにプロパティが見つかるでしょう
もう少しDaikonを使いましょう
完ぺきなパターンがあっても
このような手法は入力される実数によって決まります
Daikonが作るものはすべての実行に適していますが
平方根の事前条件にはxが0以上である場合を除き xを制限する値域がないことは分かっています
また平方根の戻り値は必ずしも 2の平方根と16の平方根の間にあるとは限りません
実際にこれは0より大きいです
つまり始点で素晴らしいテストが行われるのならば
不変条件の動的推論のツールはとても有効です
xと戻り値の正確な範囲を得る正しい方法は?
0の値で平方根を呼び出す
1の値で平方根を呼び出す
maxintの値が最大の整数である場合に maxintの値で平方根を呼び出す
負値で平方根を呼び出す
複数の呼び出しが必要です 正確な値域を得るのに必要なものを選んでください
让我给你看个例子。
一个求平方根的函数。
参数x，返回平方根。
分别用2 , 4, 16来调用。
用2来调用求平方根函数时，
我们可以知道，x的值是2，
然而，这些也是实例：
x <= 2, x >= 2,
因为这些模式对所有的值都成立。
下次迭代中，用4来调用，
x总为2的不变量已经被删掉。
我们现在只知道，x <= 4还成立。
我们可以拿前面的不变量和新的这个进行合并。
x >= 2也就仍成立了。
当我们用16来调用时，不变量就是
x <= 16 and x >= 2
最后的结果就是：
x 在2-16之间，eps总是10^-7。
对后置条件来说，也能得到类似的返回值范围。
介于2的平方根和4之间。
4就是16的平方根。
然而，还有就是，返回值的平方要等于x。
能发现这一点，是因为Daikon有一个针对这个情况的模式，
即任意两个变量的相乘 == 另一变量的模式，
它的实例化是通过两个返回值 和x，
这个模式不管如何运行程序都是成立的--
至少对于整数是这样。
如果是浮点数嘛，精度会起作用，
因为舍入错误，则这个模式就不能成立了。
所以Daikon可以得到的其实局限于它拥有的模式库，
但如果你加入更多的模式，就能发现更多的性质，
只是会让Daikon更费时一点，才能发现这些模式。
还有，即使有一个完美的模式集了，
这样的方法也要基于实际的数值，
调用的参数的值。
Daikon会把运行中发现的关联都找出来，
不过我们也知道，平方根的实际先决条件
并不由x来进行特定的限制，
除了限制下x必须>= 0。
同样，返回值也不用是2平方根到
16的平方根之间。
它可以是>= 0的任意值。
所以，不变量动态引用的工具可以很好的发挥作用，
只要在一开始就有很好的测试集。
我们应该如何得到x 和返回值正确的范围呢？
通过用0来调用 这个函数？
用1来调用？
用最大的整数来调用，
还是用负数来调用？
提示：你需要多个调用。
选择所有你认为需要的选项。交给你了。