Thank you very much, and now for the answer.
The answer is if we want to have correct ranges for the input variables
as well as for the output variables,
we need to provide these ranges when calling square root.
In our case, the correct range for x is 0 to maxint.
If we invoke square root with 0, and if we invoke square root with the maximum integer,
what we're going to get is that x is greater or equal than 0
and x is less or equal than maxint,
which is actually the correct range.
Likewise, we've learned that the return value is always greater or equal than 0,
and it's always less or equal than the square root of maxint.
If we invoke the square root with a value of 1, this won't change a lot.
We will slightly expand the range, but we won't get the 0 in here.
This is actually not needed.
If we invoke square root with -1, then we will actually violate the implicit precondition.
Let's hope that square root then will actually fail
such that Daikon can then deduce that if we invoke square root
with a negative number it fails. These two are the correct values.
Grazie mille, ed ora le risposte.
Le risposta e' che se vogliamo avere delle variabili in input entro intervalli giusti
cosi' come per le variabili di output,
abbiam bisogno di inserire questi intervalli per le chiamate a square-root.
Nel nostro caso, l'intervallo giusto per x e' tra 0 e MAXINT.
Se chiamiamo square-root(0) e square-root con l'intero maggiore,
cio' che otterremo sara' x >=0
e x <= MAXINT,
che e' effettivamente l'intervallo giusto.
Allo stesso modo, abbiamo imparato che il valore di rientro e' sempre >= 0
ed e' sempre <= della radice quadrata di MAXINT.
Se chiamassimo square-root con valore 1, non cambierebbe molto le cose,
allargheremo leggermente l'intervallo ma non avremmo lo 0 qui.
Questo non e' veramente necessario:
se chiamiamo square-root con -1 violeremo in effetti la precondizione implicita,
sperando che square-root in effetti si blocchi
di modo che Daikon riesca a dedurre che se chiamiamo square-root
con valori negativi questa si blocca. Questi due sono i valori esatti.
それでは答え合わせをしましょう
出力変数だけでなく 入力変数の正確な値域も把握したい場合は
平方根を呼び出して これらの値域を与える必要があります
この場合xの正確な値域は0からmaxintです
0で平方根を呼び出し そのあと最大数で平方根を呼び出した場合
xは0以上またはmaxint以下という結果になります
これが実際の正確な値域です
同様に戻り値は常に0以上であり
常にmaxintの平方根以下なのです
1の値で平方根を呼び出してもさほど変化はありません
少しずつ範囲を拡大していきますが 必要ないのでここでは0は取得しません
‐1で平方根を呼び出すと 暗示的事前条件は満たされなくなります
Daikonも予測しているように
負の数で平方根を呼び出した場合 失敗するでしょう
この2つが正解です
答案来了。
答案就是，如果想让输入变量有正确的范围，
输出变量也正确，
我们就需要在调用平方根函数时，进行这些范围（的检测）。
本例中，x的正确范围是0到最大的整数。
如果我们以0来调用平方根，或是用最大的整数来调用，
得到的就是x >= 0，
且<= 最大的整数，
这就是正确的范围了。
同理，已知返回值总是>= 0，
并<= 最大整数的平方根。
如果我们用1来调用的话，则没有变化（1开方还是1）。
我们可以扩展下这个范围，但不会得到0。（不明白）
实际上这个并不需要。
如果我们调用的是-1，就违反了隐含的先决条件。
希望开平方函数会失败，
这样Daikon就可以推断出，如果我们调用开平方函数时，
参数是个负数的话，就会失败。所以，这两个是正确的值。